Metamath Proof Explorer


Theorem grur1

Description: A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis gruina.1 A = U On
Assertion grur1 U Univ U R1 On U = R1 A

Proof

Step Hyp Ref Expression
1 gruina.1 A = U On
2 nss ¬ U R1 A x x U ¬ x R1 A
3 fveqeq2 y = x rank y = A rank x = A
4 3 rspcev x U rank x = A y U rank y = A
5 4 ex x U rank x = A y U rank y = A
6 5 ad2antrl U Univ U R1 On x U ¬ x R1 A rank x = A y U rank y = A
7 simplr U Univ U R1 On x U ¬ x R1 A U R1 On
8 simprl U Univ U R1 On x U ¬ x R1 A x U
9 r1elssi U R1 On U R1 On
10 9 sseld U R1 On x U x R1 On
11 7 8 10 sylc U Univ U R1 On x U ¬ x R1 A x R1 On
12 tcrank x R1 On rank x = rank TC x
13 11 12 syl U Univ U R1 On x U ¬ x R1 A rank x = rank TC x
14 13 eleq2d U Univ U R1 On x U ¬ x R1 A A rank x A rank TC x
15 gruelss U Univ x U x U
16 grutr U Univ Tr U
17 16 adantr U Univ x U Tr U
18 vex x V
19 tcmin x V x U Tr U TC x U
20 18 19 ax-mp x U Tr U TC x U
21 15 17 20 syl2anc U Univ x U TC x U
22 rankf rank : R1 On On
23 ffun rank : R1 On On Fun rank
24 22 23 ax-mp Fun rank
25 fvelima Fun rank A rank TC x y TC x rank y = A
26 24 25 mpan A rank TC x y TC x rank y = A
27 ssrexv TC x U y TC x rank y = A y U rank y = A
28 21 26 27 syl2im U Univ x U A rank TC x y U rank y = A
29 28 ad2ant2r U Univ U R1 On x U ¬ x R1 A A rank TC x y U rank y = A
30 14 29 sylbid U Univ U R1 On x U ¬ x R1 A A rank x y U rank y = A
31 simprr U Univ U R1 On x U ¬ x R1 A ¬ x R1 A
32 ne0i x U U
33 1 gruina U Univ U A Inacc
34 32 33 sylan2 U Univ x U A Inacc
35 inawina A Inacc A Inacc 𝑤
36 winaon A Inacc 𝑤 A On
37 34 35 36 3syl U Univ x U A On
38 r1fnon R1 Fn On
39 fndm R1 Fn On dom R1 = On
40 38 39 ax-mp dom R1 = On
41 37 40 eleqtrrdi U Univ x U A dom R1
42 41 ad2ant2r U Univ U R1 On x U ¬ x R1 A A dom R1
43 rankr1ag x R1 On A dom R1 x R1 A rank x A
44 11 42 43 syl2anc U Univ U R1 On x U ¬ x R1 A x R1 A rank x A
45 31 44 mtbid U Univ U R1 On x U ¬ x R1 A ¬ rank x A
46 rankon rank x On
47 eloni rank x On Ord rank x
48 eloni A On Ord A
49 ordtri3or Ord rank x Ord A rank x A rank x = A A rank x
50 47 48 49 syl2an rank x On A On rank x A rank x = A A rank x
51 46 37 50 sylancr U Univ x U rank x A rank x = A A rank x
52 3orass rank x A rank x = A A rank x rank x A rank x = A A rank x
53 51 52 sylib U Univ x U rank x A rank x = A A rank x
54 53 ord U Univ x U ¬ rank x A rank x = A A rank x
55 54 ad2ant2r U Univ U R1 On x U ¬ x R1 A ¬ rank x A rank x = A A rank x
56 45 55 mpd U Univ U R1 On x U ¬ x R1 A rank x = A A rank x
57 6 30 56 mpjaod U Univ U R1 On x U ¬ x R1 A y U rank y = A
58 57 ex U Univ U R1 On x U ¬ x R1 A y U rank y = A
59 58 exlimdv U Univ U R1 On x x U ¬ x R1 A y U rank y = A
60 2 59 syl5bi U Univ U R1 On ¬ U R1 A y U rank y = A
61 simpll U Univ U R1 On y U rank y = A U Univ
62 ne0i y U U
63 62 33 sylan2 U Univ y U A Inacc
64 63 ad2ant2r U Univ U R1 On y U rank y = A A Inacc
65 64 35 36 3syl U Univ U R1 On y U rank y = A A On
66 simprl U Univ U R1 On y U rank y = A y U
67 fveq2 rank y = A cf rank y = cf A
68 67 ad2antll U Univ U R1 On y U rank y = A cf rank y = cf A
69 elina A Inacc A cf A = A x A 𝒫 x A
70 69 simp2bi A Inacc cf A = A
71 64 70 syl U Univ U R1 On y U rank y = A cf A = A
72 68 71 eqtrd U Univ U R1 On y U rank y = A cf rank y = A
73 rankcf ¬ y cf rank y
74 fvex cf rank y V
75 vex y V
76 domtri cf rank y V y V cf rank y y ¬ y cf rank y
77 74 75 76 mp2an cf rank y y ¬ y cf rank y
78 73 77 mpbir cf rank y y
79 72 78 eqbrtrrdi U Univ U R1 On y U rank y = A A y
80 grudomon U Univ A On y U A y A U
81 61 65 66 79 80 syl112anc U Univ U R1 On y U rank y = A A U
82 elin A U On A U A On
83 82 biimpri A U A On A U On
84 83 1 eleqtrrdi A U A On A A
85 ordirr Ord A ¬ A A
86 48 85 syl A On ¬ A A
87 86 adantl A U A On ¬ A A
88 84 87 pm2.21dd A U A On U R1 A
89 81 65 88 syl2anc U Univ U R1 On y U rank y = A U R1 A
90 89 rexlimdvaa U Univ U R1 On y U rank y = A U R1 A
91 60 90 syld U Univ U R1 On ¬ U R1 A U R1 A
92 91 pm2.18d U Univ U R1 On U R1 A
93 1 grur1a U Univ R1 A U
94 93 adantr U Univ U R1 On R1 A U
95 92 94 eqssd U Univ U R1 On U = R1 A