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