| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovex 7464 | . 2
⊢
(𝒫 ∪ ran 𝐽 ↑pm dom 𝐽) ∈ V | 
| 2 |  | brssc 17858 | . . . 4
⊢ (ℎ ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) | 
| 3 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → 𝐽 Fn (𝑡 × 𝑡)) | 
| 4 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑡 ∈ V | 
| 5 | 4, 4 | xpex 7773 | . . . . . . . . . 10
⊢ (𝑡 × 𝑡) ∈ V | 
| 6 |  | fnex 7237 | . . . . . . . . . 10
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑡 × 𝑡) ∈ V) → 𝐽 ∈ V) | 
| 7 | 3, 5, 6 | sylancl 586 | . . . . . . . . 9
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → 𝐽 ∈ V) | 
| 8 |  | rnexg 7924 | . . . . . . . . 9
⊢ (𝐽 ∈ V → ran 𝐽 ∈ V) | 
| 9 |  | uniexg 7760 | . . . . . . . . 9
⊢ (ran
𝐽 ∈ V → ∪ ran 𝐽 ∈ V) | 
| 10 |  | pwexg 5378 | . . . . . . . . 9
⊢ (∪ ran 𝐽 ∈ V → 𝒫 ∪ ran 𝐽 ∈ V) | 
| 11 | 7, 8, 9, 10 | 4syl 19 | . . . . . . . 8
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → 𝒫 ∪ ran 𝐽 ∈ V) | 
| 12 |  | fndm 6671 | . . . . . . . . . 10
⊢ (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡)) | 
| 13 | 12 | adantr 480 | . . . . . . . . 9
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → dom 𝐽 = (𝑡 × 𝑡)) | 
| 14 | 13, 5 | eqeltrdi 2849 | . . . . . . . 8
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → dom 𝐽 ∈ V) | 
| 15 |  | ss2ixp 8950 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) ⊆ 𝒫 ∪ ran 𝐽 → X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥) ⊆ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ∪ ran
𝐽) | 
| 16 |  | fvssunirn 6939 | . . . . . . . . . . . . 13
⊢ (𝐽‘𝑥) ⊆ ∪ ran
𝐽 | 
| 17 | 16 | sspwi 4612 | . . . . . . . . . . . 12
⊢ 𝒫
(𝐽‘𝑥) ⊆ 𝒫 ∪ ran 𝐽 | 
| 18 | 17 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑠 × 𝑠) → 𝒫 (𝐽‘𝑥) ⊆ 𝒫 ∪ ran 𝐽) | 
| 19 | 15, 18 | mprg 3067 | . . . . . . . . . 10
⊢ X𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) ⊆ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ∪ ran
𝐽 | 
| 20 |  | simprr 773 | . . . . . . . . . 10
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) | 
| 21 | 19, 20 | sselid 3981 | . . . . . . . . 9
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ∪ ran
𝐽) | 
| 22 |  | vex 3484 | . . . . . . . . . 10
⊢ ℎ ∈ V | 
| 23 | 22 | elixpconst 8945 | . . . . . . . . 9
⊢ (ℎ ∈ X𝑥 ∈
(𝑠 × 𝑠)𝒫 ∪ ran 𝐽 ↔ ℎ:(𝑠 × 𝑠)⟶𝒫 ∪ ran 𝐽) | 
| 24 | 21, 23 | sylib 218 | . . . . . . . 8
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → ℎ:(𝑠 × 𝑠)⟶𝒫 ∪ ran 𝐽) | 
| 25 |  | elpwi 4607 | . . . . . . . . . . 11
⊢ (𝑠 ∈ 𝒫 𝑡 → 𝑠 ⊆ 𝑡) | 
| 26 | 25 | ad2antrl 728 | . . . . . . . . . 10
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → 𝑠 ⊆ 𝑡) | 
| 27 |  | xpss12 5700 | . . . . . . . . . 10
⊢ ((𝑠 ⊆ 𝑡 ∧ 𝑠 ⊆ 𝑡) → (𝑠 × 𝑠) ⊆ (𝑡 × 𝑡)) | 
| 28 | 26, 26, 27 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → (𝑠 × 𝑠) ⊆ (𝑡 × 𝑡)) | 
| 29 | 28, 13 | sseqtrrd 4021 | . . . . . . . 8
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → (𝑠 × 𝑠) ⊆ dom 𝐽) | 
| 30 |  | elpm2r 8885 | . . . . . . . 8
⊢
(((𝒫 ∪ ran 𝐽 ∈ V ∧ dom 𝐽 ∈ V) ∧ (ℎ:(𝑠 × 𝑠)⟶𝒫 ∪ ran 𝐽 ∧ (𝑠 × 𝑠) ⊆ dom 𝐽)) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) | 
| 31 | 11, 14, 24, 29, 30 | syl22anc 839 | . . . . . . 7
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) | 
| 32 | 31 | rexlimdvaa 3156 | . . . . . 6
⊢ (𝐽 Fn (𝑡 × 𝑡) → (∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽))) | 
| 33 | 32 | imp 406 | . . . . 5
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) | 
| 34 | 33 | exlimiv 1930 | . . . 4
⊢
(∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) | 
| 35 | 2, 34 | sylbi 217 | . . 3
⊢ (ℎ ⊆cat 𝐽 → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) | 
| 36 | 35 | abssi 4070 | . 2
⊢ {ℎ ∣ ℎ ⊆cat 𝐽} ⊆ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽) | 
| 37 | 1, 36 | ssexi 5322 | 1
⊢ {ℎ ∣ ℎ ⊆cat 𝐽} ∈ V |