Metamath Proof Explorer

Theorem onfrALTlem2VD

Description: Virtual deduction proof of onfrALTlem2 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem2 is onfrALTlem2VD without virtual deductions and was automatically derived from onfrALTlem2VD .

1:: |- (. ( 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 ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ).
2:1: |- (. ( 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:2: |- (. ( 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 ).
4:: |- (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
5:: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
6:5: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
7:4: |- (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
8:6,7: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
9:8: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
10:9: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Tr x ).
11:1: |- (. ( 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 ) ).
12:11: |- (. ( 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 ).
13:2: |- (. ( 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 ).
14:10,12,13: |- (. ( 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 ).
15:3,14: |- (. ( 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 ) ).
16:13,15: |- (. ( 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 ) ).
17:16: |- (. ( 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 ) ) ).
18:17: |- (. ( 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 ) ) ).
19:18: |- (. ( 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 ) ).
20:: |- (. ( 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 ) /\ ( ( a i^i x ) i^i y ) = (/) ) ).
21:20: |- (. ( 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 ) = (/) ).
22:19,21: |- (. ( 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 ) = (/) ).
23:20: |- (. ( 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 ) ).
24:23: |- (. ( 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 ).
25:22,24: |- (. ( 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 ) = (/) ) ).
26:25: |- (. ( 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 ) = (/) ) ) ).
27:26: |- (. ( 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 ) = (/) ) ) ).
28:27: |- (. ( 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 ) = (/) ) -> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) ).
29:: |- (. ( 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 ) = (/) ).
30:29: |- (. ( 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 ) = (/) ) ).
31:28,30: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y ( y e. a /\ ( a i^i y ) = (/) ) ).
qed:31: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).
(Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem2VD 
|- (. ( 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 idn3 
 |-  (. ( 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 ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ).
2 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 ) )
3 1 2 e3 
 |-  (. ( 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 ) ).
4 inss2 
 |-  ( a i^i y ) C_ y
5 4 sseli 
 |-  ( z e. ( a i^i y ) -> z e. y )
6 3 5 e3 
 |-  (. ( 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 ).
7 inss1 
 |-  ( a i^i y ) C_ a
8 7 sseli 
 |-  ( z e. ( a i^i y ) -> z e. a )
9 3 8 e3 
 |-  (. ( 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 ).
10 idn2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
11 simpl 
 |-  ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> x e. a )
12 10 11 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
13 idn1 
 |-  (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
14 simpl 
 |-  ( ( a C_ On /\ a =/= (/) ) -> a C_ On )
15 13 14 e1a 
 |-  (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
16 ssel 
 |-  ( a C_ On -> ( x e. a -> x e. On ) )
17 16 com12 
 |-  ( x e. a -> ( a C_ On -> x e. On ) )
18 12 15 17 e21 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
19 eloni 
 |-  ( x e. On -> Ord x )
20 18 19 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
21 ordtr 
 |-  ( Ord x -> Tr x )
22 20 21 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Tr x ).
23 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 ) )
24 1 23 e3 
 |-  (. ( 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 ) ).
25 inss2 
 |-  ( a i^i x ) C_ x
26 25 sseli 
 |-  ( y e. ( a i^i x ) -> y e. x )
27 24 26 e3 
 |-  (. ( 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 ).
28 trel 
 |-  ( Tr x -> ( ( z e. y /\ y e. x ) -> z e. x ) )
29 28 expcomd 
 |-  ( Tr x -> ( y e. x -> ( z e. y -> z e. x ) ) )
30 22 27 6 29 e233 
 |-  (. ( 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 ).
31 elin 
 |-  ( z e. ( a i^i x ) <-> ( z e. a /\ z e. x ) )
32 31 simplbi2 
 |-  ( z e. a -> ( z e. x -> z e. ( a i^i x ) ) )
33 9 30 32 e33 
 |-  (. ( 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 ) ).
34 elin 
 |-  ( z e. ( ( a i^i x ) i^i y ) <-> ( z e. ( a i^i x ) /\ z e. y ) )
35 34 simplbi2com 
 |-  ( z e. y -> ( z e. ( a i^i x ) -> z e. ( ( a i^i x ) i^i y ) ) )
36 6 33 35 e33 
 |-  (. ( 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 ) ).
37 36 in3an 
 |-  (. ( 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 ) ) ).
38 37 gen31 
 |-  (. ( 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 ) ) ).
39 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 ) ) )
40 39 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 ) )
41 38 40 e3 
 |-  (. ( 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 ) ).
42 idn3 
 |-  (. ( 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 ) /\ ( ( a i^i x ) i^i y ) = (/) ) ).
43 simpr 
 |-  ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( ( a i^i x ) i^i y ) = (/) )
44 42 43 e3 
 |-  (. ( 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 ) = (/) ).
45 sseq0 
 |-  ( ( ( a i^i y ) C_ ( ( a i^i x ) i^i y ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( a i^i y ) = (/) )
46 45 ex 
 |-  ( ( a i^i y ) C_ ( ( a i^i x ) i^i y ) -> ( ( ( a i^i x ) i^i y ) = (/) -> ( a i^i y ) = (/) ) )
47 41 44 46 e33 
 |-  (. ( 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 ) = (/) ).
48 simpl 
 |-  ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> y e. ( a i^i x ) )
49 42 48 e3 
 |-  (. ( 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 ) ).
50 inss1 
 |-  ( a i^i x ) C_ a
51 50 sseli 
 |-  ( y e. ( a i^i x ) -> y e. a )
52 49 51 e3 
 |-  (. ( 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 ).
53 pm3.21 
 |-  ( ( a i^i y ) = (/) -> ( y e. a -> ( y e. a /\ ( a i^i y ) = (/) ) ) )
54 47 52 53 e33 
 |-  (. ( 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 ) = (/) ) ).
55 54 in3 
 |-  (. ( 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 ) = (/) ) ) ).
56 55 gen21 
 |-  (. ( 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 ) = (/) ) ) ).
57 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 ) = (/) ) ) )
58 56 57 e2 
 |-  (. ( 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 ) = (/) ) -> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) ).
59 onfrALTlem3VD 
 |-  (. ( 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 ) = (/) ).
60 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 ) = (/) ) )
61 60 biimpi 
 |-  ( 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 ) = (/) ) )
62 59 61 e2 
 |-  (. ( 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 ) = (/) ) ).
63 id 
 |-  ( ( E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> E. 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 ) = (/) ) ) )
64 58 62 63 e22 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y ( y e. a /\ ( a i^i y ) = (/) ) ).
65 df-rex 
 |-  ( E. y e. a ( a i^i y ) = (/) <-> E. y ( y e. a /\ ( a i^i y ) = (/) ) )
66 65 biimpri 
 |-  ( E. y ( y e. a /\ ( a i^i y ) = (/) ) -> E. y e. a ( a i^i y ) = (/) )
67 64 66 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).