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 i^i On )
Assertion grur1a 
|- ( U e. Univ -> ( R1 ` A ) C_ U )

Proof

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