| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sscrel 17857 | . . 3
⊢ Rel
⊆cat | 
| 2 | 1 | brrelex12i 5740 | . 2
⊢ (𝐻 ⊆cat 𝐽 → (𝐻 ∈ V ∧ 𝐽 ∈ V)) | 
| 3 |  | vex 3484 | . . . . . 6
⊢ 𝑡 ∈ V | 
| 4 | 3, 3 | xpex 7773 | . . . . 5
⊢ (𝑡 × 𝑡) ∈ V | 
| 5 |  | fnex 7237 | . . . . 5
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑡 × 𝑡) ∈ V) → 𝐽 ∈ V) | 
| 6 | 4, 5 | mpan2 691 | . . . 4
⊢ (𝐽 Fn (𝑡 × 𝑡) → 𝐽 ∈ V) | 
| 7 |  | elex 3501 | . . . . 5
⊢ (𝐻 ∈ X𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) → 𝐻 ∈ V) | 
| 8 | 7 | rexlimivw 3151 | . . . 4
⊢
(∃𝑠 ∈
𝒫 𝑡𝐻 ∈ X𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) → 𝐻 ∈ V) | 
| 9 | 6, 8 | anim12ci 614 | . . 3
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → (𝐻 ∈ V ∧ 𝐽 ∈ V)) | 
| 10 | 9 | exlimiv 1930 | . 2
⊢
(∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → (𝐻 ∈ V ∧ 𝐽 ∈ V)) | 
| 11 |  | simpr 484 | . . . . . 6
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽) | 
| 12 | 11 | fneq1d 6661 | . . . . 5
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (𝑗 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑡 × 𝑡))) | 
| 13 |  | simpl 482 | . . . . . . 7
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → ℎ = 𝐻) | 
| 14 | 11 | fveq1d 6908 | . . . . . . . . 9
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (𝑗‘𝑥) = (𝐽‘𝑥)) | 
| 15 | 14 | pweqd 4617 | . . . . . . . 8
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → 𝒫 (𝑗‘𝑥) = 𝒫 (𝐽‘𝑥)) | 
| 16 | 15 | ixpeq2dv 8953 | . . . . . . 7
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) = X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) | 
| 17 | 13, 16 | eleq12d 2835 | . . . . . 6
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) ↔ 𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) | 
| 18 | 17 | rexbidv 3179 | . . . . 5
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥) ↔ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) | 
| 19 | 12, 18 | anbi12d 632 | . . . 4
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → ((𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)) ↔ (𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) | 
| 20 | 19 | exbidv 1921 | . . 3
⊢ ((ℎ = 𝐻 ∧ 𝑗 = 𝐽) → (∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)) ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) | 
| 21 |  | df-ssc 17854 | . . 3
⊢ 
⊆cat = {〈ℎ, 𝑗〉 ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))} | 
| 22 | 20, 21 | brabga 5539 | . 2
⊢ ((𝐻 ∈ V ∧ 𝐽 ∈ V) → (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)))) | 
| 23 | 2, 10, 22 | pm5.21nii 378 | 1
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) |