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

Theorem onfrALTlem2VD 34090
Description: Virtual deduction proof of onfrALTlem2 33712. 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 33712 is onfrALTlem2VD 34090 without virtual deductions and was automatically derived from onfrALTlem2VD 34090.
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 33795 . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . 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 33928 . . . . . . . . . . . . 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 3705 . . . . . . . . . . . . . 14  |-  ( a  i^i  y )  C_  y
54sseli 3485 . . . . . . . . . . . . 13  |-  ( z  e.  ( a  i^i  y )  ->  z  e.  y )
63, 5e3 33928 . . . . . . . . . . . 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 3704 . . . . . . . . . . . . . . 15  |-  ( a  i^i  y )  C_  a
87sseli 3485 . . . . . . . . . . . . . 14  |-  ( z  e.  ( a  i^i  y )  ->  z  e.  a )
93, 8e3 33928 . . . . . . . . . . . . 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 33793 . . . . . . . . . . . . . . . . . 18  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  ( x  e.  a  /\  -.  (
a  i^i  x )  =  (/) ) ).
11 simpl 455 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->  x  e.  a )
1210, 11e2 33811 . . . . . . . . . . . . . . . . 17  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  x  e.  a ).
13 idn1 33745 . . . . . . . . . . . . . . . . . 18  |-  (. (
a  C_  On  /\  a  =/=  (/) )  ->.  ( a  C_  On  /\  a  =/=  (/) ) ).
14 simpl 455 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  C_  On  /\  a  =/=  (/) )  ->  a  C_  On )
1513, 14e1a 33807 . . . . . . . . . . . . . . . . 17  |-  (. (
a  C_  On  /\  a  =/=  (/) )  ->.  a  C_  On ).
16 ssel 3483 . . . . . . . . . . . . . . . . . 18  |-  ( a 
C_  On  ->  ( x  e.  a  ->  x  e.  On ) )
1716com12 31 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  a  ->  (
a  C_  On  ->  x  e.  On ) )
1812, 15, 17e21 33921 . . . . . . . . . . . . . . . 16  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  x  e.  On ).
19 eloni 4877 . . . . . . . . . . . . . . . 16  |-  ( x  e.  On  ->  Ord  x )
2018, 19e2 33811 . . . . . . . . . . . . . . 15  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  Ord  x ).
21 ordtr 4881 . . . . . . . . . . . . . . 15  |-  ( Ord  x  ->  Tr  x
)
2220, 21e2 33811 . . . . . . . . . . . . . 14  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  Tr  x ).
23 simpll 751 . . . . . . . . . . . . . . . 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 33928 . . . . . . . . . . . . . . 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 3705 . . . . . . . . . . . . . . . 16  |-  ( a  i^i  x )  C_  x
2625sseli 3485 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( a  i^i  x )  ->  y  e.  x )
2724, 26e3 33928 . . . . . . . . . . . . . 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 4539 . . . . . . . . . . . . . . 15  |-  ( Tr  x  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
2928expcomd 436 . . . . . . . . . . . . . 14  |-  ( Tr  x  ->  ( y  e.  x  ->  ( z  e.  y  ->  z  e.  x ) ) )
3022, 27, 6, 29e233 33956 . . . . . . . . . . . . 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 3673 . . . . . . . . . . . . . 14  |-  ( z  e.  ( a  i^i  x )  <->  ( z  e.  a  /\  z  e.  x ) )
3231simplbi2 623 . . . . . . . . . . . . 13  |-  ( z  e.  a  ->  (
z  e.  x  -> 
z  e.  ( a  i^i  x ) ) )
339, 30, 32e33 33925 . . . . . . . . . . . 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 3673 . . . . . . . . . . . . 13  |-  ( z  e.  ( ( a  i^i  x )  i^i  y )  <->  ( z  e.  ( a  i^i  x
)  /\  z  e.  y ) )
3534simplbi2com 625 . . . . . . . . . . . 12  |-  ( z  e.  y  ->  (
z  e.  ( a  i^i  x )  -> 
z  e.  ( ( a  i^i  x )  i^i  y ) ) )
366, 33, 35e33 33925 . . . . . . . . . . 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 33791 . . . . . . . . . 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 33801 . . . . . . . . 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 3478 . . . . . . . . . 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 206 . . . . . . . . 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 33928 . . . . . . . 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 33795 . . . . . . . . 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 459 . . . . . . . . 9  |-  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y
)  =  (/) )  -> 
( ( a  i^i  x )  i^i  y
)  =  (/) )
4442, 43e3 33928 . . . . . . . 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 3816 . . . . . . . . 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 432 . . . . . . . 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 33925 . . . . . . 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 455 . . . . . . . . 9  |-  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y
)  =  (/) )  -> 
y  e.  ( a  i^i  x ) )
4942, 48e3 33928 . . . . . . . 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 3704 . . . . . . . . 9  |-  ( a  i^i  x )  C_  a
5150sseli 3485 . . . . . . . 8  |-  ( y  e.  ( a  i^i  x )  ->  y  e.  a )
5249, 51e3 33928 . . . . . . 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 446 . . . . . . 7  |-  ( ( a  i^i  y )  =  (/)  ->  ( y  e.  a  ->  (
y  e.  a  /\  ( a  i^i  y
)  =  (/) ) ) )
5447, 52, 53e33 33925 . . . . . 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 33789 . . . . 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 33799 . . . 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 1659 . . . 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 33811 . . 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 34088 . . . 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 2810 . . . . 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 194 . . . 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 33811 . . 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 22 . . 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 33851 . 2  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  E. y
( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ).
65 df-rex 2810 . . 3  |-  ( E. y  e.  a  ( a  i^i  y )  =  (/)  <->  E. y ( y  e.  a  /\  (
a  i^i  y )  =  (/) ) )
6665biimpri 206 . 2  |-  ( E. y ( y  e.  a  /\  ( a  i^i  y )  =  (/) )  ->  E. y  e.  a  ( a  i^i  y )  =  (/) )
6764, 66e2 33811 1  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  -.  ( a  i^i  x
)  =  (/) )  ->.  E. y  e.  a  ( a  i^i  y )  =  (/) ).
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367   A.wal 1396    = wceq 1398   E.wex 1617    e. wcel 1823    =/= wne 2649   E.wrex 2805    i^i cin 3460    C_ wss 3461   (/)c0 3783   Tr wtr 4532   Ord word 4866   Oncon0 4867   (.wvd2 33748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-fal 1404  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-tr 4533  df-eprel 4780  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-vd1 33741  df-vd2 33749  df-vd3 33761
This theorem is referenced by:  onfrALTVD  34092
  Copyright terms: Public domain W3C validator