Metamath Proof Explorer

Theorem sltval2

Description: Alternate expression for surreal less than. Two surreals obey surreal less than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011)

Ref Expression
Assertion sltval2 
|- ( ( A e. No /\ B e. No ) -> ( A  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )

Proof

Step Hyp Ref Expression
1 sltval 
 |-  ( ( A e. No /\ B e. No ) -> ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
2 fvex 
 |-  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. _V
3 fvex 
 |-  ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. _V
4 2 3 brtp 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) <-> ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
5 1n0 
 |-  1o =/= (/)
6 5 neii 
 |-  -. 1o = (/)
7 eqeq1 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) <-> 1o = (/) ) )
8 6 7 mtbiri 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o -> -. ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
9 fvprc 
 |-  ( -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
10 8 9 nsyl2 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
11 10 adantr 
 |-  ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
12 10 adantr 
 |-  ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
13 2on0 
 |-  2o =/= (/)
14 13 neii 
 |-  -. 2o = (/)
15 eqeq1 
 |-  ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o -> ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) <-> 2o = (/) ) )
16 14 15 mtbiri 
 |-  ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
17 fvprc 
 |-  ( -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V -> ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
18 16 17 nsyl2 
 |-  ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
19 18 adantl 
 |-  ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
20 11 12 19 3jaoi 
 |-  ( ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
21 4 20 sylbi 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
22 onintrab 
 |-  ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V <-> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
23 21 22 sylib 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
24 23 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
25 onelon 
 |-  ( ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> y e. On )
26 25 expcom 
 |-  ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On -> y e. On ) )
27 24 26 syl5 
 |-  ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> y e. On ) )
28 fveq2 
 |-  ( a = y -> ( A ` a ) = ( A ` y ) )
29 fveq2 
 |-  ( a = y -> ( B ` a ) = ( B ` y ) )
30 28 29 neeq12d 
 |-  ( a = y -> ( ( A ` a ) =/= ( B ` a ) <-> ( A ` y ) =/= ( B ` y ) ) )
31 30 onnminsb 
 |-  ( y e. On -> ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> -. ( A ` y ) =/= ( B ` y ) ) )
32 31 com12 
 |-  ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( y e. On -> -. ( A ` y ) =/= ( B ` y ) ) )
33 27 32 syldc 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> -. ( A ` y ) =/= ( B ` y ) ) )
34 df-ne 
 |-  ( ( A ` y ) =/= ( B ` y ) <-> -. ( A ` y ) = ( B ` y ) )
35 34 con2bii 
 |-  ( ( A ` y ) = ( B ` y ) <-> -. ( A ` y ) =/= ( B ` y ) )
36 33 35 syl6ibr 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> ( y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` y ) = ( B ` y ) ) )
37 36 ralrimiv 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) )
38 24 37 jca 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) ) )
39 38 ex 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) ) ) )
40 39 impac 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> ( ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
41 anass 
 |-  ( ( ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) <-> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) )
42 40 41 sylib 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) )
43 raleq 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A. y e. x ( A ` y ) = ( B ` y ) <-> A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) ) )
44 fveq2 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` x ) = ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
45 fveq2 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( B ` x ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
46 44 45 breq12d 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
47 43 46 anbi12d 
 |-  ( x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) )
48 47 rspcev 
 |-  ( ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ ( A. y e. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ( A ` y ) = ( B ` y ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) -> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
49 42 48 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) -> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
50 49 ex 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
51 eqeq12 
 |-  ( ( ( A ` x ) = 1o /\ ( B ` x ) = (/) ) -> ( ( A ` x ) = ( B ` x ) <-> 1o = (/) ) )
52 6 51 mtbiri 
 |-  ( ( ( A ` x ) = 1o /\ ( B ` x ) = (/) ) -> -. ( A ` x ) = ( B ` x ) )
53 1on 
 |-  1o e. On
54 0elon 
 |-  (/) e. On
55 suc11 
 |-  ( ( 1o e. On /\ (/) e. On ) -> ( suc 1o = suc (/) <-> 1o = (/) ) )
56 55 necon3bid 
 |-  ( ( 1o e. On /\ (/) e. On ) -> ( suc 1o =/= suc (/) <-> 1o =/= (/) ) )
57 53 54 56 mp2an 
 |-  ( suc 1o =/= suc (/) <-> 1o =/= (/) )
58 5 57 mpbir 
 |-  suc 1o =/= suc (/)
59 df-2o 
 |-  2o = suc 1o
60 df-1o 
 |-  1o = suc (/)
61 59 60 eqeq12i 
 |-  ( 2o = 1o <-> suc 1o = suc (/) )
62 58 61 nemtbir 
 |-  -. 2o = 1o
63 eqeq12 
 |-  ( ( ( A ` x ) = 1o /\ ( B ` x ) = 2o ) -> ( ( A ` x ) = ( B ` x ) <-> 1o = 2o ) )
64 eqcom 
 |-  ( 1o = 2o <-> 2o = 1o )
65 63 64 bitrdi 
 |-  ( ( ( A ` x ) = 1o /\ ( B ` x ) = 2o ) -> ( ( A ` x ) = ( B ` x ) <-> 2o = 1o ) )
66 62 65 mtbiri 
 |-  ( ( ( A ` x ) = 1o /\ ( B ` x ) = 2o ) -> -. ( A ` x ) = ( B ` x ) )
67 13 nesymi 
 |-  -. (/) = 2o
68 eqeq12 
 |-  ( ( ( A ` x ) = (/) /\ ( B ` x ) = 2o ) -> ( ( A ` x ) = ( B ` x ) <-> (/) = 2o ) )
69 67 68 mtbiri 
 |-  ( ( ( A ` x ) = (/) /\ ( B ` x ) = 2o ) -> -. ( A ` x ) = ( B ` x ) )
70 52 66 69 3jaoi 
 |-  ( ( ( ( A ` x ) = 1o /\ ( B ` x ) = (/) ) \/ ( ( A ` x ) = 1o /\ ( B ` x ) = 2o ) \/ ( ( A ` x ) = (/) /\ ( B ` x ) = 2o ) ) -> -. ( A ` x ) = ( B ` x ) )
71 fvex 
 |-  ( A ` x ) e. _V
72 fvex 
 |-  ( B ` x ) e. _V
73 71 72 brtp 
 |-  ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( ( ( A ` x ) = 1o /\ ( B ` x ) = (/) ) \/ ( ( A ` x ) = 1o /\ ( B ` x ) = 2o ) \/ ( ( A ` x ) = (/) /\ ( B ` x ) = 2o ) ) )
74 df-ne 
 |-  ( ( A ` x ) =/= ( B ` x ) <-> -. ( A ` x ) = ( B ` x ) )
75 70 73 74 3imtr4i 
 |-  ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) -> ( A ` x ) =/= ( B ` x ) )
76 fveq2 
 |-  ( a = x -> ( A ` a ) = ( A ` x ) )
77 fveq2 
 |-  ( a = x -> ( B ` a ) = ( B ` x ) )
78 76 77 neeq12d 
 |-  ( a = x -> ( ( A ` a ) =/= ( B ` a ) <-> ( A ` x ) =/= ( B ` x ) ) )
79 78 elrab 
 |-  ( x e. { a e. On | ( A ` a ) =/= ( B ` a ) } <-> ( x e. On /\ ( A ` x ) =/= ( B ` x ) ) )
80 79 biimpri 
 |-  ( ( x e. On /\ ( A ` x ) =/= ( B ` x ) ) -> x e. { a e. On | ( A ` a ) =/= ( B ` a ) } )
81 80 adantlr 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ ( A ` x ) =/= ( B ` x ) ) -> x e. { a e. On | ( A ` a ) =/= ( B ` a ) } )
82 ssrab2 
 |-  { a e. On | ( A ` a ) =/= ( B ` a ) } C_ On
83 ne0i 
 |-  ( x e. { a e. On | ( A ` a ) =/= ( B ` a ) } -> { a e. On | ( A ` a ) =/= ( B ` a ) } =/= (/) )
84 83 adantl 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> { a e. On | ( A ` a ) =/= ( B ` a ) } =/= (/) )
85 onint 
 |-  ( ( { a e. On | ( A ` a ) =/= ( B ` a ) } C_ On /\ { a e. On | ( A ` a ) =/= ( B ` a ) } =/= (/) ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. { a e. On | ( A ` a ) =/= ( B ` a ) } )
86 82 84 85 sylancr 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. { a e. On | ( A ` a ) =/= ( B ` a ) } )
87 nfrab1 
 |-  F/_ a { a e. On | ( A ` a ) =/= ( B ` a ) }
88 87 nfint 
 |-  F/_ a |^| { a e. On | ( A ` a ) =/= ( B ` a ) }
89 nfcv 
 |-  F/_ a On
90 nfcv 
 |-  F/_ a A
91 90 88 nffv 
 |-  F/_ a ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
92 nfcv 
 |-  F/_ a B
93 92 88 nffv 
 |-  F/_ a ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
94 91 93 nfne 
 |-  F/ a ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) =/= ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
95 fveq2 
 |-  ( a = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` a ) = ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
96 fveq2 
 |-  ( a = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( B ` a ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
97 95 96 neeq12d 
 |-  ( a = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A ` a ) =/= ( B ` a ) <-> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) =/= ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
98 88 89 94 97 elrabf 
 |-  ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. { a e. On | ( A ` a ) =/= ( B ` a ) } <-> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On /\ ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) =/= ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
99 98 simprbi 
 |-  ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) =/= ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
100 86 99 syl 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) =/= ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
101 df-ne 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) =/= ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) <-> -. ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
102 100 101 sylib 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> -. ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
103 fveq2 
 |-  ( y = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( A ` y ) = ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
104 fveq2 
 |-  ( y = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( B ` y ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
105 103 104 eqeq12d 
 |-  ( y = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } -> ( ( A ` y ) = ( B ` y ) <-> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
106 105 rspccv 
 |-  ( A. y e. x ( A ` y ) = ( B ` y ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. x -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
107 106 ad2antlr 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. x -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
108 102 107 mtod 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. x )
109 simpll 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> x e. On )
110 oninton 
 |-  ( ( { a e. On | ( A ` a ) =/= ( B ` a ) } C_ On /\ { a e. On | ( A ` a ) =/= ( B ` a ) } =/= (/) ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
111 82 83 110 sylancr 
 |-  ( x e. { a e. On | ( A ` a ) =/= ( B ` a ) } -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
112 111 adantl 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On )
113 ontri1 
 |-  ( ( x e. On /\ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. On ) -> ( x C_ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } <-> -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. x ) )
114 109 112 113 syl2anc 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> ( x C_ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } <-> -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. x ) )
115 108 114 mpbird 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> x C_ |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
116 intss1 
 |-  ( x e. { a e. On | ( A ` a ) =/= ( B ` a ) } -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } C_ x )
117 116 adantl 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } C_ x )
118 115 117 eqssd 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ x e. { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
119 81 118 syldan 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ ( A ` x ) =/= ( B ` x ) ) -> x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
120 75 119 sylan2 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) -> x = |^| { a e. On | ( A ` a ) =/= ( B ` a ) } )
121 120 fveq2d 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) -> ( A ` x ) = ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
122 120 fveq2d 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) -> ( B ` x ) = ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
123 121 122 breq12d 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
124 123 biimpd 
 |-  ( ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
125 124 ex 
 |-  ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) ) )
126 125 pm2.43d 
 |-  ( ( x e. On /\ A. y e. x ( A ` y ) = ( B ` y ) ) -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
127 126 expimpd 
 |-  ( x e. On -> ( ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
128 127 rexlimiv 
 |-  ( E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) )
129 50 128 impbid1 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) <-> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
130 1 129 bitr4d 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )