MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sscpwex Structured version   Visualization version   GIF version

Theorem sscpwex 17183
Description: An analogue of pwex 5244 for the subcategory subset relation: The collection of subcategory subsets of a given set 𝐽 is a set. (Contributed by Mario Carneiro, 6-Jan-2017.)
Assertion
Ref Expression
sscpwex {cat 𝐽} ∈ V
Distinct variable group:   ,𝐽

Proof of Theorem sscpwex
Dummy variables 𝑠 𝑡 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 7197 . 2 (𝒫 ran 𝐽pm dom 𝐽) ∈ V
2 brssc 17182 . . . 4 (cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥)))
3 simpl 486 . . . . . . . . . 10 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → 𝐽 Fn (𝑡 × 𝑡))
4 vex 3401 . . . . . . . . . . 11 𝑡 ∈ V
54, 4xpex 7488 . . . . . . . . . 10 (𝑡 × 𝑡) ∈ V
6 fnex 6984 . . . . . . . . . 10 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑡 × 𝑡) ∈ V) → 𝐽 ∈ V)
73, 5, 6sylancl 589 . . . . . . . . 9 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → 𝐽 ∈ V)
8 rnexg 7628 . . . . . . . . 9 (𝐽 ∈ V → ran 𝐽 ∈ V)
9 uniexg 7478 . . . . . . . . 9 (ran 𝐽 ∈ V → ran 𝐽 ∈ V)
10 pwexg 5242 . . . . . . . . 9 ( ran 𝐽 ∈ V → 𝒫 ran 𝐽 ∈ V)
117, 8, 9, 104syl 19 . . . . . . . 8 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → 𝒫 ran 𝐽 ∈ V)
12 fndm 6434 . . . . . . . . . 10 (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡))
1312adantr 484 . . . . . . . . 9 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → dom 𝐽 = (𝑡 × 𝑡))
1413, 5eqeltrdi 2841 . . . . . . . 8 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → dom 𝐽 ∈ V)
15 ss2ixp 8513 . . . . . . . . . . 11 (∀𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥) ⊆ 𝒫 ran 𝐽X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥) ⊆ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ran 𝐽)
16 fvssunirn 6697 . . . . . . . . . . . . 13 (𝐽𝑥) ⊆ ran 𝐽
1716sspwi 4499 . . . . . . . . . . . 12 𝒫 (𝐽𝑥) ⊆ 𝒫 ran 𝐽
1817a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (𝑠 × 𝑠) → 𝒫 (𝐽𝑥) ⊆ 𝒫 ran 𝐽)
1915, 18mprg 3067 . . . . . . . . . 10 X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥) ⊆ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ran 𝐽
20 simprr 773 . . . . . . . . . 10 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))
2119, 20sseldi 3873 . . . . . . . . 9 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → X𝑥 ∈ (𝑠 × 𝑠)𝒫 ran 𝐽)
22 vex 3401 . . . . . . . . . 10 ∈ V
2322elixpconst 8508 . . . . . . . . 9 (X𝑥 ∈ (𝑠 × 𝑠)𝒫 ran 𝐽:(𝑠 × 𝑠)⟶𝒫 ran 𝐽)
2421, 23sylib 221 . . . . . . . 8 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → :(𝑠 × 𝑠)⟶𝒫 ran 𝐽)
25 elpwi 4494 . . . . . . . . . . 11 (𝑠 ∈ 𝒫 𝑡𝑠𝑡)
2625ad2antrl 728 . . . . . . . . . 10 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → 𝑠𝑡)
27 xpss12 5534 . . . . . . . . . 10 ((𝑠𝑡𝑠𝑡) → (𝑠 × 𝑠) ⊆ (𝑡 × 𝑡))
2826, 26, 27syl2anc 587 . . . . . . . . 9 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → (𝑠 × 𝑠) ⊆ (𝑡 × 𝑡))
2928, 13sseqtrrd 3916 . . . . . . . 8 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → (𝑠 × 𝑠) ⊆ dom 𝐽)
30 elpm2r 8448 . . . . . . . 8 (((𝒫 ran 𝐽 ∈ V ∧ dom 𝐽 ∈ V) ∧ (:(𝑠 × 𝑠)⟶𝒫 ran 𝐽 ∧ (𝑠 × 𝑠) ⊆ dom 𝐽)) → ∈ (𝒫 ran 𝐽pm dom 𝐽))
3111, 14, 24, 29, 30syl22anc 838 . . . . . . 7 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → ∈ (𝒫 ran 𝐽pm dom 𝐽))
3231rexlimdvaa 3194 . . . . . 6 (𝐽 Fn (𝑡 × 𝑡) → (∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥) → ∈ (𝒫 ran 𝐽pm dom 𝐽)))
3332imp 410 . . . . 5 ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥)) → ∈ (𝒫 ran 𝐽pm dom 𝐽))
3433exlimiv 1936 . . . 4 (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥)) → ∈ (𝒫 ran 𝐽pm dom 𝐽))
352, 34sylbi 220 . . 3 (cat 𝐽 ∈ (𝒫 ran 𝐽pm dom 𝐽))
3635abssi 3957 . 2 {cat 𝐽} ⊆ (𝒫 ran 𝐽pm dom 𝐽)
371, 36ssexi 5187 1 {cat 𝐽} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1542  wex 1786  wcel 2113  {cab 2716  wrex 3054  Vcvv 3397  wss 3841  𝒫 cpw 4485   cuni 4793   class class class wbr 5027   × cxp 5517  dom cdm 5519  ran crn 5520   Fn wfn 6328  wf 6329  cfv 6333  (class class class)co 7164  pm cpm 8431  Xcixp 8500  cat cssc 17175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-ov 7167  df-oprab 7168  df-mpo 7169  df-pm 8433  df-ixp 8501  df-ssc 17178
This theorem is referenced by:  issubc  17203
  Copyright terms: Public domain W3C validator