Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> z e. ( a i^i y ) ) |
2 |
1
|
2a1i |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> z e. ( a i^i y ) ) ) ) |
3 |
|
inss2 |
|- ( a i^i y ) C_ y |
4 |
3
|
sseli |
|- ( z e. ( a i^i y ) -> z e. y ) |
5 |
2 4
|
syl8 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> z e. y ) ) ) |
6 |
|
inss1 |
|- ( a i^i y ) C_ a |
7 |
6
|
sseli |
|- ( z e. ( a i^i y ) -> z e. a ) |
8 |
2 7
|
syl8 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> z e. a ) ) ) |
9 |
|
simpl |
|- ( ( a C_ On /\ a =/= (/) ) -> a C_ On ) |
10 |
|
simpl |
|- ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> x e. a ) |
11 |
|
ssel |
|- ( a C_ On -> ( x e. a -> x e. On ) ) |
12 |
9 10 11
|
syl2im |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> x e. On ) ) |
13 |
|
eloni |
|- ( x e. On -> Ord x ) |
14 |
12 13
|
syl6 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> Ord x ) ) |
15 |
|
ordtr |
|- ( Ord x -> Tr x ) |
16 |
14 15
|
syl6 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> Tr x ) ) |
17 |
|
simpll |
|- ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> y e. ( a i^i x ) ) |
18 |
17
|
2a1i |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> y e. ( a i^i x ) ) ) ) |
19 |
|
inss2 |
|- ( a i^i x ) C_ x |
20 |
19
|
sseli |
|- ( y e. ( a i^i x ) -> y e. x ) |
21 |
18 20
|
syl8 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> y e. x ) ) ) |
22 |
|
trel |
|- ( Tr x -> ( ( z e. y /\ y e. x ) -> z e. x ) ) |
23 |
22
|
expcomd |
|- ( Tr x -> ( y e. x -> ( z e. y -> z e. x ) ) ) |
24 |
16 21 5 23
|
ee233 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> z e. x ) ) ) |
25 |
|
elin |
|- ( z e. ( a i^i x ) <-> ( z e. a /\ z e. x ) ) |
26 |
25
|
simplbi2 |
|- ( z e. a -> ( z e. x -> z e. ( a i^i x ) ) ) |
27 |
8 24 26
|
ee33 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> z e. ( a i^i x ) ) ) ) |
28 |
|
elin |
|- ( z e. ( ( a i^i x ) i^i y ) <-> ( z e. ( a i^i x ) /\ z e. y ) ) |
29 |
28
|
simplbi2com |
|- ( z e. y -> ( z e. ( a i^i x ) -> z e. ( ( a i^i x ) i^i y ) ) ) |
30 |
5 27 29
|
ee33 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) -> z e. ( ( a i^i x ) i^i y ) ) ) ) |
31 |
30
|
exp4a |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ) ) ) |
32 |
31
|
ggen31 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> A. z ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ) ) ) |
33 |
|
dfss2 |
|- ( ( a i^i y ) C_ ( ( a i^i x ) i^i y ) <-> A. z ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ) |
34 |
33
|
biimpri |
|- ( A. z ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) -> ( a i^i y ) C_ ( ( a i^i x ) i^i y ) ) |
35 |
32 34
|
syl8 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( a i^i y ) C_ ( ( a i^i x ) i^i y ) ) ) ) |
36 |
|
simpr |
|- ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( ( a i^i x ) i^i y ) = (/) ) |
37 |
36
|
2a1i |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( ( a i^i x ) i^i y ) = (/) ) ) ) |
38 |
|
sseq0 |
|- ( ( ( a i^i y ) C_ ( ( a i^i x ) i^i y ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( a i^i y ) = (/) ) |
39 |
38
|
ex |
|- ( ( a i^i y ) C_ ( ( a i^i x ) i^i y ) -> ( ( ( a i^i x ) i^i y ) = (/) -> ( a i^i y ) = (/) ) ) |
40 |
35 37 39
|
ee33 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( a i^i y ) = (/) ) ) ) |
41 |
|
simpl |
|- ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> y e. ( a i^i x ) ) |
42 |
41
|
2a1i |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> y e. ( a i^i x ) ) ) ) |
43 |
|
inss1 |
|- ( a i^i x ) C_ a |
44 |
43
|
sseli |
|- ( y e. ( a i^i x ) -> y e. a ) |
45 |
42 44
|
syl8 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> y e. a ) ) ) |
46 |
|
pm3.21 |
|- ( ( a i^i y ) = (/) -> ( y e. a -> ( y e. a /\ ( a i^i y ) = (/) ) ) ) |
47 |
40 45 46
|
ee33 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) ) ) |
48 |
47
|
alrimdv |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> A. y ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) ) ) |
49 |
|
onfrALTlem3 |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) ) |
50 |
|
df-rex |
|- ( E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) |
51 |
49 50
|
syl6ib |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) ) |
52 |
|
exim |
|- ( A. y ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) -> ( E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) ) |
53 |
48 51 52
|
syl6c |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) ) |
54 |
|
df-rex |
|- ( E. y e. a ( a i^i y ) = (/) <-> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) |
55 |
53 54
|
syl6ibr |
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> E. y e. a ( a i^i y ) = (/) ) ) |