Step | Hyp | Ref
| Expression |
1 | | sscrel 16473 |
. . 3
⊢ Rel
⊆cat |
2 | | brrelex12 5155 |
. . 3
⊢ ((Rel
⊆cat ∧ 𝐻 ⊆cat 𝐽) → (𝐻 ∈ V ∧ 𝐽 ∈ V)) |
3 | 1, 2 | mpan 706 |
. 2
⊢ (𝐻 ⊆cat 𝐽 → (𝐻 ∈ V ∧ 𝐽 ∈ V)) |
4 | | vex 3203 |
. . . . . 6
⊢ 𝑡 ∈ V |
5 | 4, 4 | xpex 6962 |
. . . . 5
⊢ (𝑡 × 𝑡) ∈ V |
6 | | fnex 6481 |
. . . . 5
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑡 × 𝑡) ∈ V) → 𝐽 ∈ V) |
7 | 5, 6 | mpan2 707 |
. . . 4
⊢ (𝐽 Fn (𝑡 × 𝑡) → 𝐽 ∈ V) |
8 | | elex 3212 |
. . . . 5
⊢ (𝐻 ∈ X𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) → 𝐻 ∈ V) |
9 | 8 | rexlimivw 3029 |
. . . 4
⊢
(∃𝑠 ∈
𝒫 𝑡𝐻 ∈ X𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) → 𝐻 ∈ V) |
10 | 7, 9 | anim12ci 591 |
. . 3
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → (𝐻 ∈ V ∧ 𝐽 ∈ V)) |
11 | 10 | exlimiv 1858 |
. 2
⊢
(∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → (𝐻 ∈ V ∧ 𝐽 ∈ V)) |
12 | | simpr 477 |
. . . . . 6
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽) |
13 | 12 | fneq1d 5981 |
. . . . 5
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (𝑗 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑡 × 𝑡))) |
14 | | simpl 473 |
. . . . . . 7
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → ℎ = 𝐻) |
15 | 12 | fveq1d 6193 |
. . . . . . . . 9
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (𝑗‘𝑥) = (𝐽‘𝑥)) |
16 | 15 | pweqd 4163 |
. . . . . . . 8
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → 𝒫 (𝑗‘𝑥) = 𝒫 (𝐽‘𝑥)) |
17 | 16 | ixpeq2dv 7924 |
. . . . . . 7
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) = X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) |
18 | 14, 17 | eleq12d 2695 |
. . . . . 6
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) ↔ 𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) |
19 | 18 | rexbidv 3052 |
. . . . 5
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) ↔ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) |
20 | 13, 19 | anbi12d 747 |
. . . 4
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → ((𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)) ↔ (𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) |
21 | 20 | exbidv 1850 |
. . 3
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)) ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) |
22 | | df-ssc 16470 |
. . 3
⊢
⊆cat = {〈ℎ, 𝑗〉 ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))} |
23 | 21, 22 | brabga 4989 |
. 2
⊢ ((𝐻 ∈ V ∧ 𝐽 ∈ V) → (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) |
24 | 3, 11, 23 | pm5.21nii 368 |
1
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) |