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

Theorem grur1 10811
Description: A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.)
Hypothesis
Ref Expression
gruina.1 𝐴 = (𝑈 ∩ On)
Assertion
Ref Expression
grur1 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → 𝑈 = (𝑅1𝐴))

Proof of Theorem grur1
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nss 4045 . . . . 5 𝑈 ⊆ (𝑅1𝐴) ↔ ∃𝑥(𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴)))
2 fveqeq2 6897 . . . . . . . . . . 11 (𝑦 = 𝑥 → ((rank‘𝑦) = 𝐴 ↔ (rank‘𝑥) = 𝐴))
32rspcev 3612 . . . . . . . . . 10 ((𝑥𝑈 ∧ (rank‘𝑥) = 𝐴) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴)
43ex 414 . . . . . . . . 9 (𝑥𝑈 → ((rank‘𝑥) = 𝐴 → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
54ad2antrl 727 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ((rank‘𝑥) = 𝐴 → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
6 simplr 768 . . . . . . . . . . . 12 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → 𝑈 (𝑅1 “ On))
7 simprl 770 . . . . . . . . . . . 12 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → 𝑥𝑈)
8 r1elssi 9796 . . . . . . . . . . . . 13 (𝑈 (𝑅1 “ On) → 𝑈 (𝑅1 “ On))
98sseld 3980 . . . . . . . . . . . 12 (𝑈 (𝑅1 “ On) → (𝑥𝑈𝑥 (𝑅1 “ On)))
106, 7, 9sylc 65 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → 𝑥 (𝑅1 “ On))
11 tcrank 9875 . . . . . . . . . . 11 (𝑥 (𝑅1 “ On) → (rank‘𝑥) = (rank “ (TC‘𝑥)))
1210, 11syl 17 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (rank‘𝑥) = (rank “ (TC‘𝑥)))
1312eleq2d 2820 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (𝐴 ∈ (rank‘𝑥) ↔ 𝐴 ∈ (rank “ (TC‘𝑥))))
14 gruelss 10785 . . . . . . . . . . . 12 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝑥𝑈)
15 grutr 10784 . . . . . . . . . . . . 13 (𝑈 ∈ Univ → Tr 𝑈)
1615adantr 482 . . . . . . . . . . . 12 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → Tr 𝑈)
17 vex 3479 . . . . . . . . . . . . 13 𝑥 ∈ V
18 tcmin 9732 . . . . . . . . . . . . 13 (𝑥 ∈ V → ((𝑥𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈))
1917, 18ax-mp 5 . . . . . . . . . . . 12 ((𝑥𝑈 ∧ Tr 𝑈) → (TC‘𝑥) ⊆ 𝑈)
2014, 16, 19syl2anc 585 . . . . . . . . . . 11 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (TC‘𝑥) ⊆ 𝑈)
21 rankf 9785 . . . . . . . . . . . . 13 rank: (𝑅1 “ On)⟶On
22 ffun 6717 . . . . . . . . . . . . 13 (rank: (𝑅1 “ On)⟶On → Fun rank)
2321, 22ax-mp 5 . . . . . . . . . . . 12 Fun rank
24 fvelima 6954 . . . . . . . . . . . 12 ((Fun rank ∧ 𝐴 ∈ (rank “ (TC‘𝑥))) → ∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴)
2523, 24mpan 689 . . . . . . . . . . 11 (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴)
26 ssrexv 4050 . . . . . . . . . . 11 ((TC‘𝑥) ⊆ 𝑈 → (∃𝑦 ∈ (TC‘𝑥)(rank‘𝑦) = 𝐴 → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
2720, 25, 26syl2im 40 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
2827ad2ant2r 746 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (𝐴 ∈ (rank “ (TC‘𝑥)) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
2913, 28sylbid 239 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (𝐴 ∈ (rank‘𝑥) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
30 simprr 772 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ¬ 𝑥 ∈ (𝑅1𝐴))
31 ne0i 4333 . . . . . . . . . . . . . . 15 (𝑥𝑈𝑈 ≠ ∅)
32 gruina.1 . . . . . . . . . . . . . . . 16 𝐴 = (𝑈 ∩ On)
3332gruina 10809 . . . . . . . . . . . . . . 15 ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
3431, 33sylan2 594 . . . . . . . . . . . . . 14 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ Inacc)
35 inawina 10681 . . . . . . . . . . . . . 14 (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
36 winaon 10679 . . . . . . . . . . . . . 14 (𝐴 ∈ Inaccw𝐴 ∈ On)
3734, 35, 363syl 18 . . . . . . . . . . . . 13 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ On)
38 r1fnon 9758 . . . . . . . . . . . . . 14 𝑅1 Fn On
39 fndm 6649 . . . . . . . . . . . . . 14 (𝑅1 Fn On → dom 𝑅1 = On)
4038, 39ax-mp 5 . . . . . . . . . . . . 13 dom 𝑅1 = On
4137, 40eleqtrrdi 2845 . . . . . . . . . . . 12 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → 𝐴 ∈ dom 𝑅1)
4241ad2ant2r 746 . . . . . . . . . . 11 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → 𝐴 ∈ dom 𝑅1)
43 rankr1ag 9793 . . . . . . . . . . 11 ((𝑥 (𝑅1 “ On) ∧ 𝐴 ∈ dom 𝑅1) → (𝑥 ∈ (𝑅1𝐴) ↔ (rank‘𝑥) ∈ 𝐴))
4410, 42, 43syl2anc 585 . . . . . . . . . 10 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (𝑥 ∈ (𝑅1𝐴) ↔ (rank‘𝑥) ∈ 𝐴))
4530, 44mtbid 324 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ¬ (rank‘𝑥) ∈ 𝐴)
46 rankon 9786 . . . . . . . . . . . . 13 (rank‘𝑥) ∈ On
47 eloni 6371 . . . . . . . . . . . . . 14 ((rank‘𝑥) ∈ On → Ord (rank‘𝑥))
48 eloni 6371 . . . . . . . . . . . . . 14 (𝐴 ∈ On → Ord 𝐴)
49 ordtri3or 6393 . . . . . . . . . . . . . 14 ((Ord (rank‘𝑥) ∧ Ord 𝐴) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)))
5047, 48, 49syl2an 597 . . . . . . . . . . . . 13 (((rank‘𝑥) ∈ On ∧ 𝐴 ∈ On) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)))
5146, 37, 50sylancr 588 . . . . . . . . . . . 12 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)))
52 3orass 1091 . . . . . . . . . . . 12 (((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)) ↔ ((rank‘𝑥) ∈ 𝐴 ∨ ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥))))
5351, 52sylib 217 . . . . . . . . . . 11 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → ((rank‘𝑥) ∈ 𝐴 ∨ ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥))))
5453ord 863 . . . . . . . . . 10 ((𝑈 ∈ Univ ∧ 𝑥𝑈) → (¬ (rank‘𝑥) ∈ 𝐴 → ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥))))
5554ad2ant2r 746 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → (¬ (rank‘𝑥) ∈ 𝐴 → ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥))))
5645, 55mpd 15 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ((rank‘𝑥) = 𝐴𝐴 ∈ (rank‘𝑥)))
575, 29, 56mpjaod 859 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴))) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴)
5857ex 414 . . . . . 6 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → ((𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴)) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
5958exlimdv 1937 . . . . 5 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (∃𝑥(𝑥𝑈 ∧ ¬ 𝑥 ∈ (𝑅1𝐴)) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
601, 59biimtrid 241 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (¬ 𝑈 ⊆ (𝑅1𝐴) → ∃𝑦𝑈 (rank‘𝑦) = 𝐴))
61 simpll 766 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑈 ∈ Univ)
62 ne0i 4333 . . . . . . . . . 10 (𝑦𝑈𝑈 ≠ ∅)
6362, 33sylan2 594 . . . . . . . . 9 ((𝑈 ∈ Univ ∧ 𝑦𝑈) → 𝐴 ∈ Inacc)
6463ad2ant2r 746 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ Inacc)
6564, 35, 363syl 18 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴 ∈ On)
66 simprl 770 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑦𝑈)
67 fveq2 6888 . . . . . . . . . 10 ((rank‘𝑦) = 𝐴 → (cf‘(rank‘𝑦)) = (cf‘𝐴))
6867ad2antll 728 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = (cf‘𝐴))
69 elina 10678 . . . . . . . . . . 11 (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴 𝒫 𝑥𝐴))
7069simp2bi 1147 . . . . . . . . . 10 (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
7164, 70syl 17 . . . . . . . . 9 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘𝐴) = 𝐴)
7268, 71eqtrd 2773 . . . . . . . 8 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → (cf‘(rank‘𝑦)) = 𝐴)
73 rankcf 10768 . . . . . . . . 9 ¬ 𝑦 ≺ (cf‘(rank‘𝑦))
74 fvex 6901 . . . . . . . . . 10 (cf‘(rank‘𝑦)) ∈ V
75 vex 3479 . . . . . . . . . 10 𝑦 ∈ V
76 domtri 10547 . . . . . . . . . 10 (((cf‘(rank‘𝑦)) ∈ V ∧ 𝑦 ∈ V) → ((cf‘(rank‘𝑦)) ≼ 𝑦 ↔ ¬ 𝑦 ≺ (cf‘(rank‘𝑦))))
7774, 75, 76mp2an 691 . . . . . . . . 9 ((cf‘(rank‘𝑦)) ≼ 𝑦 ↔ ¬ 𝑦 ≺ (cf‘(rank‘𝑦)))
7873, 77mpbir 230 . . . . . . . 8 (cf‘(rank‘𝑦)) ≼ 𝑦
7972, 78eqbrtrrdi 5187 . . . . . . 7 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴𝑦)
80 grudomon 10808 . . . . . . 7 ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝑦𝑈𝐴𝑦)) → 𝐴𝑈)
8161, 65, 66, 79, 80syl112anc 1375 . . . . . 6 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝐴𝑈)
82 elin 3963 . . . . . . . . 9 (𝐴 ∈ (𝑈 ∩ On) ↔ (𝐴𝑈𝐴 ∈ On))
8382biimpri 227 . . . . . . . 8 ((𝐴𝑈𝐴 ∈ On) → 𝐴 ∈ (𝑈 ∩ On))
8483, 32eleqtrrdi 2845 . . . . . . 7 ((𝐴𝑈𝐴 ∈ On) → 𝐴𝐴)
85 ordirr 6379 . . . . . . . . 9 (Ord 𝐴 → ¬ 𝐴𝐴)
8648, 85syl 17 . . . . . . . 8 (𝐴 ∈ On → ¬ 𝐴𝐴)
8786adantl 483 . . . . . . 7 ((𝐴𝑈𝐴 ∈ On) → ¬ 𝐴𝐴)
8884, 87pm2.21dd 194 . . . . . 6 ((𝐴𝑈𝐴 ∈ On) → 𝑈 ⊆ (𝑅1𝐴))
8981, 65, 88syl2anc 585 . . . . 5 (((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) ∧ (𝑦𝑈 ∧ (rank‘𝑦) = 𝐴)) → 𝑈 ⊆ (𝑅1𝐴))
9089rexlimdvaa 3157 . . . 4 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (∃𝑦𝑈 (rank‘𝑦) = 𝐴𝑈 ⊆ (𝑅1𝐴)))
9160, 90syld 47 . . 3 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (¬ 𝑈 ⊆ (𝑅1𝐴) → 𝑈 ⊆ (𝑅1𝐴)))
9291pm2.18d 127 . 2 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → 𝑈 ⊆ (𝑅1𝐴))
9332grur1a 10810 . . 3 (𝑈 ∈ Univ → (𝑅1𝐴) ⊆ 𝑈)
9493adantr 482 . 2 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → (𝑅1𝐴) ⊆ 𝑈)
9592, 94eqssd 3998 1 ((𝑈 ∈ Univ ∧ 𝑈 (𝑅1 “ On)) → 𝑈 = (𝑅1𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3o 1087   = wceq 1542  wex 1782  wcel 2107  wne 2941  wral 3062  wrex 3071  Vcvv 3475  cin 3946  wss 3947  c0 4321  𝒫 cpw 4601   cuni 4907   class class class wbr 5147  Tr wtr 5264  dom cdm 5675  cima 5678  Ord word 6360  Oncon0 6361  Fun wfun 6534   Fn wfn 6535  wf 6536  cfv 6540  cdom 8933  csdm 8934  TCctc 9727  𝑅1cr1 9753  rankcrnk 9754  cfccf 9928  Inaccwcwina 10673  Inacccina 10674  Univcgru 10781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-ac2 10454
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-tc 9728  df-r1 9755  df-rank 9756  df-card 9930  df-cf 9932  df-acn 9933  df-ac 10107  df-wina 10675  df-ina 10676  df-gru 10782
This theorem is referenced by:  grutsk  10813  bj-grur1  35882  grurankcld  42925
  Copyright terms: Public domain W3C validator