Metamath Proof Explorer


Theorem onfrALTlem2

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem2
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> E. y e. a ( a i^i y ) = (/) ) )

Proof

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 ) = (/) ) )