Metamath Proof Explorer

Theorem onfrALTlem3VD

Description: Virtual deduction proof of onfrALTlem3 . 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. onfrALTlem3 is onfrALTlem3VD without virtual deductions and was automatically derived from onfrALTlem3VD .

1:: |- (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
2:: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
3:2: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
4:1: |- (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
5:3,4: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
6:5: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
7:6: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->.E We x ).
8:: |- ( a i^i x ) C x
9:7,8: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->.E We ( a i^i x ) ).
10:9: |- (. ( a C On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->.E Fr ( a i^i x ) ).
11:10: |- (. ( a C On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. A. b ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ).
12:: |- x e.V
13:12,8: |- ( a i^i x ) e. V
14:13,11: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ).
15:: |- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
16:14,15: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) ).
17:: |- ( a i^i x ) C_ ( a i^i x )
18:2: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. -. ( a i^i x ) = (/) ).
19:18: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( a i^i x ) =/= (/) ).
20:17,19: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) ).
qed:16,20: |- (. ( 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 ) = (/) ).
(Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 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 ) = (/) ).

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 inss2 
 |-  ( a i^i x ) C_ x
3 1 2 ssexi 
 |-  ( a i^i x ) e. _V
4 idn2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
5 simpl 
 |-  ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> x e. a )
6 4 5 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
7 idn1 
 |-  (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
8 simpl 
 |-  ( ( a C_ On /\ a =/= (/) ) -> a C_ On )
9 7 8 e1a 
 |-  (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
10 ssel 
 |-  ( a C_ On -> ( x e. a -> x e. On ) )
11 10 com12 
 |-  ( x e. a -> ( a C_ On -> x e. On ) )
12 6 9 11 e21 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
13 eloni 
 |-  ( x e. On -> Ord x )
14 12 13 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
15 ordwe 
 |-  ( Ord x -> _E We x )
16 14 15 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. _E We x ).
17 wess 
 |-  ( ( a i^i x ) C_ x -> ( _E We x -> _E We ( a i^i x ) ) )
18 17 com12 
 |-  ( _E We x -> ( ( a i^i x ) C_ x -> _E We ( a i^i x ) ) )
19 16 2 18 e20 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. _E We ( a i^i x ) ).
20 wefr 
 |-  ( _E We ( a i^i x ) -> _E Fr ( a i^i x ) )
21 19 20 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. _E Fr ( a i^i x ) ).
22 dfepfr 
 |-  ( _E Fr ( a i^i x ) <-> A. b ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) )
23 22 biimpi 
 |-  ( _E Fr ( a i^i x ) -> A. b ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) )
24 21 23 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. A. b ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ).
25 spsbc 
 |-  ( ( a i^i x ) e. _V -> ( A. b ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) -> [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ) )
26 3 24 25 e02 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ).
27 onfrALTlem5 
 |-  ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
28 26 27 e2bi 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) ).
29 ssid 
 |-  ( a i^i x ) C_ ( a i^i x )
30 simpr 
 |-  ( ( x e. a /\ -. ( a i^i x ) = (/) ) -> -. ( a i^i x ) = (/) )
31 4 30 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. -. ( a i^i x ) = (/) ).
32 df-ne 
 |-  ( ( a i^i x ) =/= (/) <-> -. ( a i^i x ) = (/) )
33 32 biimpri 
 |-  ( -. ( a i^i x ) = (/) -> ( a i^i x ) =/= (/) )
34 31 33 e2 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( a i^i x ) =/= (/) ).
35 pm3.2 
 |-  ( ( a i^i x ) C_ ( a i^i x ) -> ( ( a i^i x ) =/= (/) -> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) ) )
36 29 34 35 e02 
 |-  (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) ).
37 id 
 |-  ( ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) -> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
38 28 36 37 e22 
 |-  (. ( 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 ) = (/) ).