This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sscpwex

Description: An analogue of pwex for the subcategory subset relation: The collection of subcategory subsets of a given set J is a set. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion sscpwex { ℎ ∣ ℎ ⊆cat 𝐽 } ∈ V

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( 𝒫 ∪ ran 𝐽 ↑pm dom 𝐽 ) ∈ V
2 brssc ⊢ ( ℎ ⊆cat 𝐽 ↔ ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) )
3 simpl ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → 𝐽 Fn ( 𝑡 × 𝑡 ) )
4 vex ⊢ 𝑡 ∈ V
5 4 4 xpex ⊢ ( 𝑡 × 𝑡 ) ∈ V
6 fnex ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑡 × 𝑡 ) ∈ V ) → 𝐽 ∈ V )
7 3 5 6 sylancl ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → 𝐽 ∈ V )
8 rnexg ⊢ ( 𝐽 ∈ V → ran 𝐽 ∈ V )
9 uniexg ⊢ ( ran 𝐽 ∈ V → ∪ ran 𝐽 ∈ V )
10 pwexg ⊢ ( ∪ ran 𝐽 ∈ V → 𝒫 ∪ ran 𝐽 ∈ V )
11 7 8 9 10 4syl ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → 𝒫 ∪ ran 𝐽 ∈ V )
12 fndm ⊢ ( 𝐽 Fn ( 𝑡 × 𝑡 ) → dom 𝐽 = ( 𝑡 × 𝑡 ) )
13 12 adantr ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → dom 𝐽 = ( 𝑡 × 𝑡 ) )
14 13 5 eqeltrdi ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → dom 𝐽 ∈ V )
15 ss2ixp ⊢ ( ∀ 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ⊆ 𝒫 ∪ ran 𝐽 → X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ⊆ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ∪ ran 𝐽 )
16 fvssunirn ⊢ ( 𝐽 ‘ 𝑥 ) ⊆ ∪ ran 𝐽
17 16 sspwi ⊢ 𝒫 ( 𝐽 ‘ 𝑥 ) ⊆ 𝒫 ∪ ran 𝐽
18 17 a1i ⊢ ( 𝑥 ∈ ( 𝑠 × 𝑠 ) → 𝒫 ( 𝐽 ‘ 𝑥 ) ⊆ 𝒫 ∪ ran 𝐽 )
19 15 18 mprg ⊢ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ⊆ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ∪ ran 𝐽
20 simprr ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) )
21 19 20 sselid ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ∪ ran 𝐽 )
22 vex ⊢ ℎ ∈ V
23 22 elixpconst ⊢ ( ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ∪ ran 𝐽 ↔ ℎ : ( 𝑠 × 𝑠 ) ⟶ 𝒫 ∪ ran 𝐽 )
24 21 23 sylib ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → ℎ : ( 𝑠 × 𝑠 ) ⟶ 𝒫 ∪ ran 𝐽 )
25 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝑡 → 𝑠 ⊆ 𝑡 )
26 25 ad2antrl ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → 𝑠 ⊆ 𝑡 )
27 xpss12 ⊢ ( ( 𝑠 ⊆ 𝑡 ∧ 𝑠 ⊆ 𝑡 ) → ( 𝑠 × 𝑠 ) ⊆ ( 𝑡 × 𝑡 ) )
28 26 26 27 syl2anc ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → ( 𝑠 × 𝑠 ) ⊆ ( 𝑡 × 𝑡 ) )
29 28 13 sseqtrrd ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → ( 𝑠 × 𝑠 ) ⊆ dom 𝐽 )
30 elpm2r ⊢ ( ( ( 𝒫 ∪ ran 𝐽 ∈ V ∧ dom 𝐽 ∈ V ) ∧ ( ℎ : ( 𝑠 × 𝑠 ) ⟶ 𝒫 ∪ ran 𝐽 ∧ ( 𝑠 × 𝑠 ) ⊆ dom 𝐽 ) ) → ℎ ∈ ( 𝒫 ∪ ran 𝐽 ↑pm dom 𝐽 ) )
31 11 14 24 29 30 syl22anc ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ( 𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) ) → ℎ ∈ ( 𝒫 ∪ ran 𝐽 ↑pm dom 𝐽 ) )
32 31 rexlimdvaa ⊢ ( 𝐽 Fn ( 𝑡 × 𝑡 ) → ( ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) → ℎ ∈ ( 𝒫 ∪ ran 𝐽 ↑pm dom 𝐽 ) ) )
33 32 imp ⊢ ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) → ℎ ∈ ( 𝒫 ∪ ran 𝐽 ↑pm dom 𝐽 ) )
34 33 exlimiv ⊢ ( ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) → ℎ ∈ ( 𝒫 ∪ ran 𝐽 ↑pm dom 𝐽 ) )
35 2 34 sylbi ⊢ ( ℎ ⊆cat 𝐽 → ℎ ∈ ( 𝒫 ∪ ran 𝐽 ↑pm dom 𝐽 ) )
36 35 abssi ⊢ { ℎ ∣ ℎ ⊆cat 𝐽 } ⊆ ( 𝒫 ∪ ran 𝐽 ↑pm dom 𝐽 )
37 1 36 ssexi ⊢ { ℎ ∣ ℎ ⊆cat 𝐽 } ∈ V