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

Theorem grudomon 9892
Description: Each ordinal that is comparable with an element of the universe is in the universe. (Contributed by Mario Carneiro, 10-Jun-2013.)
Assertion
Ref Expression
grudomon ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝐵𝑈𝐴𝐵)) → 𝐴𝑈)

Proof of Theorem grudomon
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 4812 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐵𝑦𝐵))
2 eleq1 2832 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝑈𝑦𝑈))
31, 2imbi12d 335 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐵𝑥𝑈) ↔ (𝑦𝐵𝑦𝑈)))
43imbi2d 331 . . . . . 6 (𝑥 = 𝑦 → (((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑥𝐵𝑥𝑈)) ↔ ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑦𝐵𝑦𝑈))))
5 breq1 4812 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 eleq1 2832 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥𝑈𝐴𝑈))
75, 6imbi12d 335 . . . . . . 7 (𝑥 = 𝐴 → ((𝑥𝐵𝑥𝑈) ↔ (𝐴𝐵𝐴𝑈)))
87imbi2d 331 . . . . . 6 (𝑥 = 𝐴 → (((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑥𝐵𝑥𝑈)) ↔ ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝐴𝐵𝐴𝑈))))
9 r19.21v 3107 . . . . . . 7 (∀𝑦𝑥 ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑦𝐵𝑦𝑈)) ↔ ((𝑈 ∈ Univ ∧ 𝐵𝑈) → ∀𝑦𝑥 (𝑦𝐵𝑦𝑈)))
10 simpl1 1242 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → 𝑥 ∈ On)
11 vex 3353 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
12 onelss 5950 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ On → (𝑦𝑥𝑦𝑥))
1312imp 395 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦𝑥)
14 ssdomg 8206 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ V → (𝑦𝑥𝑦𝑥))
1511, 13, 14mpsyl 68 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦𝑥)
1610, 15sylan 575 . . . . . . . . . . . . . . 15 ((((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) ∧ 𝑦𝑥) → 𝑦𝑥)
17 simplr 785 . . . . . . . . . . . . . . 15 ((((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) ∧ 𝑦𝑥) → 𝑥𝐵)
18 domtr 8213 . . . . . . . . . . . . . . 15 ((𝑦𝑥𝑥𝐵) → 𝑦𝐵)
1916, 17, 18syl2anc 579 . . . . . . . . . . . . . 14 ((((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) ∧ 𝑦𝑥) → 𝑦𝐵)
20 pm2.27 42 . . . . . . . . . . . . . 14 (𝑦𝐵 → ((𝑦𝐵𝑦𝑈) → 𝑦𝑈))
2119, 20syl 17 . . . . . . . . . . . . 13 ((((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) ∧ 𝑦𝑥) → ((𝑦𝐵𝑦𝑈) → 𝑦𝑈))
2221ralimdva 3109 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → (∀𝑦𝑥 (𝑦𝐵𝑦𝑈) → ∀𝑦𝑥 𝑦𝑈))
23 dfss3 3750 . . . . . . . . . . . . 13 (𝑥𝑈 ↔ ∀𝑦𝑥 𝑦𝑈)
24 domeng 8174 . . . . . . . . . . . . . . . 16 (𝐵𝑈 → (𝑥𝐵 ↔ ∃𝑦(𝑥𝑦𝑦𝐵)))
25243ad2ant3 1165 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑥𝐵 ↔ ∃𝑦(𝑥𝑦𝑦𝐵)))
2625biimpa 468 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → ∃𝑦(𝑥𝑦𝑦𝐵))
27 simpl2 1244 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → 𝑈 ∈ Univ)
28 gruss 9871 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 ∈ Univ ∧ 𝐵𝑈𝑦𝐵) → 𝑦𝑈)
29283expia 1150 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑦𝐵𝑦𝑈))
30293adant1 1160 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑦𝐵𝑦𝑈))
3130adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → (𝑦𝐵𝑦𝑈))
32 ensym 8209 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑦𝑦𝑥)
3332a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → (𝑥𝑦𝑦𝑥))
3431, 33anim12d 602 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → ((𝑦𝐵𝑥𝑦) → (𝑦𝑈𝑦𝑥)))
3534ancomsd 457 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → ((𝑥𝑦𝑦𝐵) → (𝑦𝑈𝑦𝑥)))
3635eximdv 2012 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → (∃𝑦(𝑥𝑦𝑦𝐵) → ∃𝑦(𝑦𝑈𝑦𝑥)))
37 gruen 9887 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ Univ ∧ 𝑥𝑈 ∧ (𝑦𝑈𝑦𝑥)) → 𝑥𝑈)
38373com23 1156 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ Univ ∧ (𝑦𝑈𝑦𝑥) ∧ 𝑥𝑈) → 𝑥𝑈)
39383exp 1148 . . . . . . . . . . . . . . . 16 (𝑈 ∈ Univ → ((𝑦𝑈𝑦𝑥) → (𝑥𝑈𝑥𝑈)))
4039exlimdv 2028 . . . . . . . . . . . . . . 15 (𝑈 ∈ Univ → (∃𝑦(𝑦𝑈𝑦𝑥) → (𝑥𝑈𝑥𝑈)))
4127, 36, 40sylsyld 61 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → (∃𝑦(𝑥𝑦𝑦𝐵) → (𝑥𝑈𝑥𝑈)))
4226, 41mpd 15 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → (𝑥𝑈𝑥𝑈))
4323, 42syl5bir 234 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → (∀𝑦𝑥 𝑦𝑈𝑥𝑈))
4422, 43syld 47 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) ∧ 𝑥𝐵) → (∀𝑦𝑥 (𝑦𝐵𝑦𝑈) → 𝑥𝑈))
4544ex 401 . . . . . . . . . 10 ((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑥𝐵 → (∀𝑦𝑥 (𝑦𝐵𝑦𝑈) → 𝑥𝑈)))
4645com23 86 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑈 ∈ Univ ∧ 𝐵𝑈) → (∀𝑦𝑥 (𝑦𝐵𝑦𝑈) → (𝑥𝐵𝑥𝑈)))
47463expib 1152 . . . . . . . 8 (𝑥 ∈ On → ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (∀𝑦𝑥 (𝑦𝐵𝑦𝑈) → (𝑥𝐵𝑥𝑈))))
4847a2d 29 . . . . . . 7 (𝑥 ∈ On → (((𝑈 ∈ Univ ∧ 𝐵𝑈) → ∀𝑦𝑥 (𝑦𝐵𝑦𝑈)) → ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑥𝐵𝑥𝑈))))
499, 48syl5bi 233 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥 ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑦𝐵𝑦𝑈)) → ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝑥𝐵𝑥𝑈))))
504, 8, 49tfis3 7255 . . . . 5 (𝐴 ∈ On → ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝐴𝐵𝐴𝑈)))
5150com3l 89 . . . 4 ((𝑈 ∈ Univ ∧ 𝐵𝑈) → (𝐴𝐵 → (𝐴 ∈ On → 𝐴𝑈)))
5251impr 446 . . 3 ((𝑈 ∈ Univ ∧ (𝐵𝑈𝐴𝐵)) → (𝐴 ∈ On → 𝐴𝑈))
53523impia 1145 . 2 ((𝑈 ∈ Univ ∧ (𝐵𝑈𝐴𝐵) ∧ 𝐴 ∈ On) → 𝐴𝑈)
54533com23 1156 1 ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝐵𝑈𝐴𝐵)) → 𝐴𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wral 3055  Vcvv 3350  wss 3732   class class class wbr 4809  Oncon0 5908  cen 8157  cdom 8158  Univcgru 9865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-ord 5911  df-on 5912  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-gru 9866
This theorem is referenced by:  gruina  9893  grur1  9895
  Copyright terms: Public domain W3C validator