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 df-ss 
 |-  ( ( 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 imbitrdi 
 |-  ( ( 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 imbitrrdi 
 |-  ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> E. y e. a ( a i^i y ) = (/) ) )