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

Theorem sscpwex 17077
Description: An analogue of pwex 5277 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 7184 . 2 (𝒫 ran 𝐽pm dom 𝐽) ∈ V
2 brssc 17076 . . . 4 (cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥)))
3 simpl 483 . . . . . . . . . 10 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → 𝐽 Fn (𝑡 × 𝑡))
4 vex 3502 . . . . . . . . . . 11 𝑡 ∈ V
54, 4xpex 7468 . . . . . . . . . 10 (𝑡 × 𝑡) ∈ V
6 fnex 6978 . . . . . . . . . 10 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑡 × 𝑡) ∈ V) → 𝐽 ∈ V)
73, 5, 6sylancl 586 . . . . . . . . 9 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → 𝐽 ∈ V)
8 rnexg 7605 . . . . . . . . 9 (𝐽 ∈ V → ran 𝐽 ∈ V)
9 uniexg 7460 . . . . . . . . 9 (ran 𝐽 ∈ V → ran 𝐽 ∈ V)
10 pwexg 5275 . . . . . . . . 9 ( ran 𝐽 ∈ V → 𝒫 ran 𝐽 ∈ V)
117, 8, 9, 104syl 19 . . . . . . . 8 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → 𝒫 ran 𝐽 ∈ V)
12 fndm 6451 . . . . . . . . . 10 (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡))
1312adantr 481 . . . . . . . . 9 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → dom 𝐽 = (𝑡 × 𝑡))
1413, 5syl6eqel 2925 . . . . . . . 8 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → dom 𝐽 ∈ V)
15 ss2ixp 8466 . . . . . . . . . . 11 (∀𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥) ⊆ 𝒫 ran 𝐽X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥) ⊆ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ran 𝐽)
16 fvssunirn 6695 . . . . . . . . . . . . 13 (𝐽𝑥) ⊆ ran 𝐽
17 sspwb 5337 . . . . . . . . . . . . 13 ((𝐽𝑥) ⊆ ran 𝐽 ↔ 𝒫 (𝐽𝑥) ⊆ 𝒫 ran 𝐽)
1816, 17mpbi 231 . . . . . . . . . . . 12 𝒫 (𝐽𝑥) ⊆ 𝒫 ran 𝐽
1918a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (𝑠 × 𝑠) → 𝒫 (𝐽𝑥) ⊆ 𝒫 ran 𝐽)
2015, 19mprg 3156 . . . . . . . . . 10 X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥) ⊆ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ran 𝐽
21 simprr 769 . . . . . . . . . 10 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))
2220, 21sseldi 3968 . . . . . . . . 9 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → X𝑥 ∈ (𝑠 × 𝑠)𝒫 ran 𝐽)
23 vex 3502 . . . . . . . . . 10 ∈ V
2423elixpconst 8461 . . . . . . . . 9 (X𝑥 ∈ (𝑠 × 𝑠)𝒫 ran 𝐽:(𝑠 × 𝑠)⟶𝒫 ran 𝐽)
2522, 24sylib 219 . . . . . . . 8 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → :(𝑠 × 𝑠)⟶𝒫 ran 𝐽)
26 elpwi 4553 . . . . . . . . . . 11 (𝑠 ∈ 𝒫 𝑡𝑠𝑡)
2726ad2antrl 724 . . . . . . . . . 10 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → 𝑠𝑡)
28 xpss12 5568 . . . . . . . . . 10 ((𝑠𝑡𝑠𝑡) → (𝑠 × 𝑠) ⊆ (𝑡 × 𝑡))
2927, 27, 28syl2anc 584 . . . . . . . . 9 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → (𝑠 × 𝑠) ⊆ (𝑡 × 𝑡))
3029, 13sseqtrrd 4011 . . . . . . . 8 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → (𝑠 × 𝑠) ⊆ dom 𝐽)
31 elpm2r 8417 . . . . . . . 8 (((𝒫 ran 𝐽 ∈ V ∧ dom 𝐽 ∈ V) ∧ (:(𝑠 × 𝑠)⟶𝒫 ran 𝐽 ∧ (𝑠 × 𝑠) ⊆ dom 𝐽)) → ∈ (𝒫 ran 𝐽pm dom 𝐽))
3211, 14, 25, 30, 31syl22anc 836 . . . . . . 7 ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥))) → ∈ (𝒫 ran 𝐽pm dom 𝐽))
3332rexlimdvaa 3289 . . . . . 6 (𝐽 Fn (𝑡 × 𝑡) → (∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥) → ∈ (𝒫 ran 𝐽pm dom 𝐽)))
3433imp 407 . . . . 5 ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥)) → ∈ (𝒫 ran 𝐽pm dom 𝐽))
3534exlimiv 1924 . . . 4 (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑥)) → ∈ (𝒫 ran 𝐽pm dom 𝐽))
362, 35sylbi 218 . . 3 (cat 𝐽 ∈ (𝒫 ran 𝐽pm dom 𝐽))
3736abssi 4049 . 2 {cat 𝐽} ⊆ (𝒫 ran 𝐽pm dom 𝐽)
381, 37ssexi 5222 1 {cat 𝐽} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1530  wex 1773  wcel 2107  {cab 2803  wrex 3143  Vcvv 3499  wss 3939  𝒫 cpw 4541   cuni 4836   class class class wbr 5062   × cxp 5551  dom cdm 5553  ran crn 5554   Fn wfn 6346  wf 6347  cfv 6351  (class class class)co 7151  pm cpm 8400  Xcixp 8453  cat cssc 17069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-ov 7154  df-oprab 7155  df-mpo 7156  df-pm 8402  df-ixp 8454  df-ssc 17072
This theorem is referenced by:  issubc  17097
  Copyright terms: Public domain W3C validator