Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  onfrALTlem2VD Unicode version

Theorem onfrALTlem2VD 28714
Description: Virtual deduction proof of onfrALTlem2 28347. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem2 28347 is onfrALTlem2VD 28714 without virtual deductions and was automatically derived from onfrALTlem2VD 28714.
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.)
Assertion
Ref Expression
onfrALTlem2VD  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  E. y  e.  a  ( a  i^i  y )  =  (/) ).
Distinct variable groups:    y, a    x, y

Proof of Theorem onfrALTlem2VD
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 idn3 28429 . . . . . . . . . . . . . 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 ) )  ->.  ( ( y  e.  ( a  i^i  x )  /\  (
( a  i^i  x
)  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y
) ) ).
2 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) )
31, 2e3 28562 . . . . . . . . . . . . 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.  ( a  i^i  y ) ).
4 inss2 3526 . . . . . . . . . . . . . 14  |-  ( a  i^i  y )  C_  y
54sseli 3308 . . . . . . . . . . . . 13  |-  ( z  e.  ( a  i^i  y )  ->  z  e.  y )
63, 5e3 28562 . . . . . . . . . . . 12  |-  (. (
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 3525 . . . . . . . . . . . . . . 15  |-  ( a  i^i  y )  C_  a
87sseli 3308 . . . . . . . . . . . . . 14  |-  ( z  e.  ( a  i^i  y )  ->  z  e.  a )
93, 8e3 28562 . . . . . . . . . . . . 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.  a ).
10 idn2 28427 . . . . . . . . . . . . . . . . . 18  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  ( x  e.  a  /\  -.  (
a  i^i  x )  =  (/) ) ).
11 simpl 444 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->  x  e.  a )
1210, 11e2 28445 . . . . . . . . . . . . . . . . 17  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  x  e.  a ).
13 idn1 28378 . . . . . . . . . . . . . . . . . 18  |-  (. (
a  C_  On  /\  a  =/=  (/) )  ->.  ( a  C_  On  /\  a  =/=  (/) ) ).
14 simpl 444 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  C_  On  /\  a  =/=  (/) )  ->  a  C_  On )
1513, 14e1_ 28441 . . . . . . . . . . . . . . . . 17  |-  (. (
a  C_  On  /\  a  =/=  (/) )  ->.  a  C_  On ).
16 ssel 3306 . . . . . . . . . . . . . . . . . 18  |-  ( a 
C_  On  ->  ( x  e.  a  ->  x  e.  On ) )
1716com12 29 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  a  ->  (
a  C_  On  ->  x  e.  On ) )
1812, 15, 17e21 28555 . . . . . . . . . . . . . . . 16  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  x  e.  On ).
19 eloni 4555 . . . . . . . . . . . . . . . 16  |-  ( x  e.  On  ->  Ord  x )
2018, 19e2 28445 . . . . . . . . . . . . . . 15  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  Ord  x ).
21 ordtr 4559 . . . . . . . . . . . . . . 15  |-  ( Ord  x  ->  Tr  x
)
2220, 21e2 28445 . . . . . . . . . . . . . 14  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  Tr  x ).
23 simpll 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) )
241, 23e3 28562 . . . . . . . . . . . . . . 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 ) )  ->.  y  e.  ( a  i^i  x ) ).
25 inss2 3526 . . . . . . . . . . . . . . . 16  |-  ( a  i^i  x )  C_  x
2625sseli 3308 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( a  i^i  x )  ->  y  e.  x )
2724, 26e3 28562 . . . . . . . . . . . . . 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 ) )  ->.  y  e.  x ).
28 trel 4273 . . . . . . . . . . . . . . 15  |-  ( Tr  x  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
2928exp3acom23 1378 . . . . . . . . . . . . . 14  |-  ( Tr  x  ->  ( y  e.  x  ->  ( z  e.  y  ->  z  e.  x ) ) )
3022, 27, 6, 29e233 28590 . . . . . . . . . . . . 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 ).
31 elin 3494 . . . . . . . . . . . . . 14  |-  ( z  e.  ( a  i^i  x )  <->  ( z  e.  a  /\  z  e.  x ) )
3231simplbi2 609 . . . . . . . . . . . . 13  |-  ( z  e.  a  ->  (
z  e.  x  -> 
z  e.  ( a  i^i  x ) ) )
339, 30, 32e33 28559 . . . . . . . . . . . 12  |-  (. (
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 3494 . . . . . . . . . . . . 13  |-  ( z  e.  ( ( a  i^i  x )  i^i  y )  <->  ( z  e.  ( a  i^i  x
)  /\  z  e.  y ) )
3534simplbi2com 1380 . . . . . . . . . . . 12  |-  ( z  e.  y  ->  (
z  e.  ( a  i^i  x )  -> 
z  e.  ( ( a  i^i  x )  i^i  y ) ) )
366, 33, 35e33 28559 . . . . . . . . . . 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 ) )  ->.  z  e.  ( ( a  i^i  x
)  i^i  y ) ).
3736in3an 28425 . . . . . . . . . 10  |-  (. (
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 )
) ).
3837gen31 28435 . . . . . . . . 9  |-  (. (
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 3301 . . . . . . . . . 10  |-  ( ( 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 )
) )
4039biimpri 198 . . . . . . . . 9  |-  ( 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
) )
4138, 40e3 28562 . . . . . . . 8  |-  (. (
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 28429 . . . . . . . . 9  |-  (. (
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 448 . . . . . . . . 9  |-  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y
)  =  (/) )  -> 
( ( a  i^i  x )  i^i  y
)  =  (/) )
4442, 43e3 28562 . . . . . . . 8  |-  (. (
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 3623 . . . . . . . . 9  |-  ( ( ( a  i^i  y
)  C_  ( (
a  i^i  x )  i^i  y )  /\  (
( a  i^i  x
)  i^i  y )  =  (/) )  ->  (
a  i^i  y )  =  (/) )
4645ex 424 . . . . . . . 8  |-  ( ( a  i^i  y ) 
C_  ( ( a  i^i  x )  i^i  y )  ->  (
( ( a  i^i  x )  i^i  y
)  =  (/)  ->  (
a  i^i  y )  =  (/) ) )
4741, 44, 46e33 28559 . . . . . . 7  |-  (. (
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 444 . . . . . . . . 9  |-  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y
)  =  (/) )  -> 
y  e.  ( a  i^i  x ) )
4942, 48e3 28562 . . . . . . . 8  |-  (. (
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 3525 . . . . . . . . 9  |-  ( a  i^i  x )  C_  a
5150sseli 3308 . . . . . . . 8  |-  ( y  e.  ( a  i^i  x )  ->  y  e.  a )
5249, 51e3 28562 . . . . . . 7  |-  (. (
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 436 . . . . . . 7  |-  ( ( a  i^i  y )  =  (/)  ->  ( y  e.  a  ->  (
y  e.  a  /\  ( a  i^i  y
)  =  (/) ) ) )
5447, 52, 53e33 28559 . . . . . 6  |-  (. (
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 )  =  (/) ) ).
5554in3 28423 . . . . 5  |-  (. (
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 )  =  (/) ) ) ).
5655gen21 28433 . . . 4  |-  (. (
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 1581 . . . 4  |-  ( 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 )  =  (/) ) ) )
5856, 57e2 28445 . . 3  |-  (. (
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 28712 . . . 4  |-  (. (
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 2676 . . . . 5  |-  ( 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 )  =  (/) ) )
6160biimpi 187 . . . 4  |-  ( 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 )  =  (/) ) )
6259, 61e2 28445 . . 3  |-  (. (
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 20 . . 3  |-  ( ( 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 )  =  (/) ) ) )
6458, 62, 63e22 28485 . 2  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  E. y
( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ).
65 df-rex 2676 . . 3  |-  ( E. y  e.  a  ( a  i^i  y )  =  (/)  <->  E. y ( y  e.  a  /\  (
a  i^i  y )  =  (/) ) )
6665biimpri 198 . 2  |-  ( E. y ( y  e.  a  /\  ( a  i^i  y )  =  (/) )  ->  E. y  e.  a  ( a  i^i  y )  =  (/) )
6764, 66e2 28445 1  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  E. y  e.  a  ( a  i^i  y )  =  (/) ).
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1721    =/= wne 2571   E.wrex 2671    i^i cin 3283    C_ wss 3284   (/)c0 3592   Tr wtr 4266   Ord word 4544   Oncon0 4545   (.wvd2 28382
This theorem is referenced by:  onfrALTVD  28716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-tr 4267  df-eprel 4458  df-po 4467  df-so 4468  df-fr 4505  df-we 4507  df-ord 4548  df-on 4549  df-vd1 28374  df-vd2 28383  df-vd3 28395
  Copyright terms: Public domain W3C validator