Metamath Proof Explorer


Theorem grur1a

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

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

Proof

Step Hyp Ref Expression
1 gruina.1 A = U On
2 inss1 U On U
3 1 2 eqsstri A U
4 sseq2 U = A U A
5 3 4 mpbii U = A
6 ss0 A A =
7 fveq2 A = R1 A = R1
8 r10 R1 =
9 7 8 eqtrdi A = R1 A =
10 0ss U
11 9 10 eqsstrdi A = R1 A U
12 5 6 11 3syl U = R1 A U
13 12 a1i U Univ U = R1 A U
14 1 gruina U Univ U A Inacc
15 inawina A Inacc A Inacc 𝑤
16 winaon A Inacc 𝑤 A On
17 winalim A Inacc 𝑤 Lim A
18 r1lim A On Lim A R1 A = x A R1 x
19 16 17 18 syl2anc A Inacc 𝑤 R1 A = x A R1 x
20 14 15 19 3syl U Univ U R1 A = x A R1 x
21 inss2 U On On
22 1 21 eqsstri A On
23 22 sseli x A x On
24 eleq1 x = x A A
25 fveq2 x = R1 x = R1
26 25 8 eqtrdi x = R1 x =
27 26 eleq1d x = R1 x U U
28 24 27 imbi12d x = x A R1 x U A U
29 eleq1 x = y x A y A
30 fveq2 x = y R1 x = R1 y
31 30 eleq1d x = y R1 x U R1 y U
32 29 31 imbi12d x = y x A R1 x U y A R1 y U
33 eleq1 x = suc y x A suc y A
34 fveq2 x = suc y R1 x = R1 suc y
35 34 eleq1d x = suc y R1 x U R1 suc y U
36 33 35 imbi12d x = suc y x A R1 x U suc y A R1 suc y U
37 3 sseli A U
38 37 a1i U Univ A U
39 simpr U Univ suc y A suc y A
40 elelsuc suc y A suc y suc A
41 3 sseli suc y A suc y U
42 41 ne0d suc y A U
43 14 15 16 3syl U Univ U A On
44 42 43 sylan2 U Univ suc y A A On
45 eloni A On Ord A
46 ordsucelsuc Ord A y A suc y suc A
47 44 45 46 3syl U Univ suc y A y A suc y suc A
48 40 47 syl5ibr U Univ suc y A suc y A y A
49 39 48 mpd U Univ suc y A y A
50 grupw U Univ R1 y U 𝒫 R1 y U
51 50 ex U Univ R1 y U 𝒫 R1 y U
52 51 adantr U Univ suc y A R1 y U 𝒫 R1 y U
53 r1suc y On R1 suc y = 𝒫 R1 y
54 53 eleq1d y On R1 suc y U 𝒫 R1 y U
55 54 biimprcd 𝒫 R1 y U y On R1 suc y U
56 52 55 syl6 U Univ suc y A R1 y U y On R1 suc y U
57 49 56 embantd U Univ suc y A y A R1 y U y On R1 suc y U
58 57 ex U Univ suc y A y A R1 y U y On R1 suc y U
59 58 com23 U Univ y A R1 y U suc y A y On R1 suc y U
60 59 com4r y On U Univ y A R1 y U suc y A R1 suc y U
61 simpr U Univ x A x A
62 3 sseli x A x U
63 62 ne0d x A U
64 63 43 sylan2 U Univ x A A On
65 ontr1 A On y x x A y A
66 pm2.27 y A y A R1 y U R1 y U
67 65 66 syl6 A On y x x A y A R1 y U R1 y U
68 67 expd A On y x x A y A R1 y U R1 y U
69 68 com3r x A A On y x y A R1 y U R1 y U
70 61 64 69 sylc U Univ x A y x y A R1 y U R1 y U
71 70 imp U Univ x A y x y A R1 y U R1 y U
72 71 ralimdva U Univ x A y x y A R1 y U y x R1 y U
73 gruiun U Univ x U y x R1 y U y x R1 y U
74 73 3expia U Univ x U y x R1 y U y x R1 y U
75 62 74 sylan2 U Univ x A y x R1 y U y x R1 y U
76 72 75 syld U Univ x A y x y A R1 y U y x R1 y U
77 vex x V
78 r1lim x V Lim x R1 x = y x R1 y
79 77 78 mpan Lim x R1 x = y x R1 y
80 79 eleq1d Lim x R1 x U y x R1 y U
81 80 biimprd Lim x y x R1 y U R1 x U
82 76 81 sylan9r Lim x U Univ x A y x y A R1 y U R1 x U
83 82 exp32 Lim x U Univ x A y x y A R1 y U R1 x U
84 83 com34 Lim x U Univ y x y A R1 y U x A R1 x U
85 28 32 36 38 60 84 tfinds2 x On U Univ x A R1 x U
86 85 com3r x A x On U Univ R1 x U
87 23 86 mpd x A U Univ R1 x U
88 87 impcom U Univ x A R1 x U
89 gruelss U Univ R1 x U R1 x U
90 88 89 syldan U Univ x A R1 x U
91 90 ralrimiva U Univ x A R1 x U
92 iunss x A R1 x U x A R1 x U
93 91 92 sylibr U Univ x A R1 x U
94 93 adantr U Univ U x A R1 x U
95 20 94 eqsstrd U Univ U R1 A U
96 95 ex U Univ U R1 A U
97 13 96 pm2.61dne U Univ R1 A U