Step | Hyp | Ref
| Expression |
1 | | sscrel 16296 |
. . 3
⊢ Rel
⊆cat |
2 | | brrelex12 5079 |
. . 3
⊢ ((Rel
⊆cat ∧ 𝐻 ⊆cat 𝐽) → (𝐻 ∈ V ∧ 𝐽 ∈ V)) |
3 | 1, 2 | mpan 702 |
. 2
⊢ (𝐻 ⊆cat 𝐽 → (𝐻 ∈ V ∧ 𝐽 ∈ V)) |
4 | | vex 3176 |
. . . . . 6
⊢ 𝑡 ∈ V |
5 | 4, 4 | xpex 6860 |
. . . . 5
⊢ (𝑡 × 𝑡) ∈ V |
6 | | fnex 6386 |
. . . . 5
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑡 × 𝑡) ∈ V) → 𝐽 ∈ V) |
7 | 5, 6 | mpan2 703 |
. . . 4
⊢ (𝐽 Fn (𝑡 × 𝑡) → 𝐽 ∈ V) |
8 | | elex 3185 |
. . . . 5
⊢ (𝐻 ∈ X𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) → 𝐻 ∈ V) |
9 | 8 | rexlimivw 3011 |
. . . 4
⊢
(∃𝑠 ∈
𝒫 𝑡𝐻 ∈ X𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) → 𝐻 ∈ V) |
10 | 7, 9 | anim12ci 589 |
. . 3
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → (𝐻 ∈ V ∧ 𝐽 ∈ V)) |
11 | 10 | exlimiv 1845 |
. 2
⊢
(∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → (𝐻 ∈ V ∧ 𝐽 ∈ V)) |
12 | | simpr 476 |
. . . . . 6
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽) |
13 | 12 | fneq1d 5895 |
. . . . 5
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (𝑗 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑡 × 𝑡))) |
14 | | simpl 472 |
. . . . . . 7
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → ℎ = 𝐻) |
15 | 12 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (𝑗‘𝑥) = (𝐽‘𝑥)) |
16 | 15 | pweqd 4113 |
. . . . . . . 8
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → 𝒫 (𝑗‘𝑥) = 𝒫 (𝐽‘𝑥)) |
17 | 16 | ixpeq2dv 7810 |
. . . . . . 7
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) = X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) |
18 | 14, 17 | eleq12d 2682 |
. . . . . 6
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) ↔ 𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) |
19 | 18 | rexbidv 3034 |
. . . . 5
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) ↔ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) |
20 | 13, 19 | anbi12d 743 |
. . . 4
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → ((𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)) ↔ (𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) |
21 | 20 | exbidv 1837 |
. . 3
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)) ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) |
22 | | df-ssc 16293 |
. . 3
⊢
⊆cat = {〈ℎ, 𝑗〉 ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))} |
23 | 21, 22 | brabga 4914 |
. 2
⊢ ((𝐻 ∈ V ∧ 𝐽 ∈ V) → (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) |
24 | 3, 11, 23 | pm5.21nii 367 |
1
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) |