Metamath Proof Explorer

Theorem sltres

Description: If the restrictions of two surreals to a given ordinal obey surreal less-than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011)

Ref Expression
Assertion sltres 
|- ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  A

Proof

Step Hyp Ref Expression
1 noreson 
 |-  ( ( A e. No /\ X e. On ) -> ( A |` X ) e. No )
2 1 3adant2 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( A |` X ) e. No )
3 noreson 
 |-  ( ( B e. No /\ X e. On ) -> ( B |` X ) e. No )
4 3 3adant1 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( B |` X ) e. No )
5 sltintdifex 
 |-  ( ( ( A |` X ) e. No /\ ( B |` X ) e. No ) -> ( ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. _V ) )
6 onintrab 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. _V <-> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On )
7 5 6 imbitrdi 
 |-  ( ( ( A |` X ) e. No /\ ( B |` X ) e. No ) -> ( ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On ) )
8 2 4 7 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On ) )
9 8 imp 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On )
10 simpl3 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  X e. On )
11 sltval2 
 |-  ( ( ( A |` X ) e. No /\ ( B |` X ) e. No ) -> ( ( A |` X )  ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
12 2 4 11 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
13 fvex 
 |-  ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. _V
14 fvex 
 |-  ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. _V
15 13 14 brtp 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) <-> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) )
16 1n0 
 |-  1o =/= (/)
17 16 neii 
 |-  -. 1o = (/)
18 eqeq1 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) <-> 1o = (/) ) )
19 17 18 mtbiri 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> -. ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
20 ndmfv 
 |-  ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
21 19 20 nsyl2 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
22 21 adantr 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
23 22 orcd 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
24 21 adantr 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
25 24 orcd 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
26 2on 
 |-  2o e. On
27 26 elexi 
 |-  2o e. _V
28 27 prid2 
 |-  2o e. { 1o , 2o }
29 28 nosgnn0i 
 |-  (/) =/= 2o
30 29 neii 
 |-  -. (/) = 2o
31 eqeq1 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) <-> 2o = (/) ) )
32 eqcom 
 |-  ( 2o = (/) <-> (/) = 2o )
33 31 32 bitrdi 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) <-> (/) = 2o ) )
34 30 33 mtbiri 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> -. ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
35 ndmfv 
 |-  ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
36 34 35 nsyl2 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
37 36 adantl 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
38 37 olcd 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
39 23 25 38 3jaoi 
 |-  ( ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
40 15 39 sylbi 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
41 12 40 biimtrdi 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) ) )
42 41 imp 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
43 dmres 
 |-  dom ( A |` X ) = ( X i^i dom A )
44 43 elin2 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) <-> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X /\ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A ) )
45 44 simplbi 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
46 dmres 
 |-  dom ( B |` X ) = ( X i^i dom B )
47 46 elin2 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) <-> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X /\ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B ) )
48 47 simplbi 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
49 45 48 jaoi 
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) \/ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
50 42 49 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
51 onelss 
 |-  ( X e. On -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } C_ X ) )
52 10 50 51 sylc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } C_ X )
53 52 sselda 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  y e. X )
54 onelon 
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> y e. On )
55 9 54 sylan 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  y e. On )
56 intss1 
 |-  ( y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } C_ y )
57 ontri1 
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ y e. On ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } C_ y <-> -. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
58 56 57 imbitrid 
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ y e. On ) -> ( y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> -. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
59 58 con2d 
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ y e. On ) -> ( y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
60 9 59 sylan 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
61 60 impancom 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( y e. On -> -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
62 55 61 mpd 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } )
63 fveq2 
 |-  ( a = y -> ( ( A |` X ) ` a ) = ( ( A |` X ) ` y ) )
64 fveq2 
 |-  ( a = y -> ( ( B |` X ) ` a ) = ( ( B |` X ) ` y ) )
65 63 64 neeq12d 
 |-  ( a = y -> ( ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) <-> ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) ) )
66 65 elrab 
 |-  ( y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } <-> ( y e. On /\ ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) ) )
67 66 simplbi2 
 |-  ( y e. On -> ( ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) -> y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
68 67 con3d 
 |-  ( y e. On -> ( -. y e. { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> -. ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) ) )
69 55 62 68 sylc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  -. ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) )
70 df-ne 
 |-  ( ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) <-> -. ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) )
71 70 con2bii 
 |-  ( ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) <-> -. ( ( A |` X ) ` y ) =/= ( ( B |` X ) ` y ) )
72 69 71 sylibr 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) )
73 fvres 
 |-  ( y e. X -> ( ( A |` X ) ` y ) = ( A ` y ) )
74 fvres 
 |-  ( y e. X -> ( ( B |` X ) ` y ) = ( B ` y ) )
75 73 74 eqeq12d 
 |-  ( y e. X -> ( ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) <-> ( A ` y ) = ( B ` y ) ) )
76 75 biimpd 
 |-  ( y e. X -> ( ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) -> ( A ` y ) = ( B ` y ) ) )
77 53 72 76 sylc 
 |-  ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( A ` y ) = ( B ` y ) )
78 77 ralrimiva 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  A. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ( A ` y ) = ( B ` y ) )
79 fvresval 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) \/ ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
80 79 ori 
 |-  ( -. ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
81 19 80 nsyl2 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
82 81 eqcomd 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
83 eqeq2 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) <-> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o ) )
84 82 83 mpbid 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o )
85 84 adantr 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o )
86 85 a1i 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o ) )
87 21 ad2antrl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
88 87 45 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
89 nofun 
 |-  ( ( B |` X ) e. No -> Fun ( B |` X ) )
90 fvelrn 
 |-  ( ( Fun ( B |` X ) /\ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( B |` X ) )
91 90 ex 
 |-  ( Fun ( B |` X ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( B |` X ) ) )
92 89 91 syl 
 |-  ( ( B |` X ) e. No -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( B |` X ) ) )
93 norn 
 |-  ( ( B |` X ) e. No -> ran ( B |` X ) C_ { 1o , 2o } )
94 93 sseld 
 |-  ( ( B |` X ) e. No -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } ) )
95 92 94 syld 
 |-  ( ( B |` X ) e. No -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } ) )
96 nosgnn0 
 |-  -. (/) e. { 1o , 2o }
97 eleq1 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } <-> (/) e. { 1o , 2o } ) )
98 96 97 mtbiri 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } )
99 95 98 nsyli 
 |-  ( ( B |` X ) e. No -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
100 4 99 syl 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
101 100 imp 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
102 101 adantrl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
103 47 simplbi2 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) ) )
104 103 con3d 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B ) )
105 88 102 104 sylc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B )
106 ndmfv 
 |-  ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom B -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
107 105 106 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
108 107 ex 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) )
109 86 108 jcad 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) ) )
110 fvresval 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) \/ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
111 110 ori 
 |-  ( -. ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
112 34 111 nsyl2 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
113 112 eqcomd 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
114 eqeq2 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) <-> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) )
115 113 114 mpbid 
 |-  ( ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o )
116 84 115 anim12i 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) )
117 116 a1i 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) )
118 36 ad2antll 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( B |` X ) )
119 118 48 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X )
120 nofun 
 |-  ( ( A |` X ) e. No -> Fun ( A |` X ) )
121 fvelrn 
 |-  ( ( Fun ( A |` X ) /\ |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( A |` X ) )
122 121 ex 
 |-  ( Fun ( A |` X ) -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( A |` X ) ) )
123 120 122 syl 
 |-  ( ( A |` X ) e. No -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( A |` X ) ) )
124 norn 
 |-  ( ( A |` X ) e. No -> ran ( A |` X ) C_ { 1o , 2o } )
125 124 sseld 
 |-  ( ( A |` X ) e. No -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. ran ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } ) )
126 123 125 syld 
 |-  ( ( A |` X ) e. No -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } ) )
127 eleq1 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } <-> (/) e. { 1o , 2o } ) )
128 96 127 mtbiri 
 |-  ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. { 1o , 2o } )
129 126 128 nsyli 
 |-  ( ( A |` X ) e. No -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) ) )
130 2 129 syl 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) ) )
131 130 imp 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
132 131 adantrr 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) )
133 44 simplbi2 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A -> |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) ) )
134 133 con3d 
 |-  ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. X -> ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom ( A |` X ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A ) )
135 119 132 134 sylc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A )
136 135 ex 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A ) )
137 ndmfv 
 |-  ( -. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. dom A -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) )
138 136 137 syl6 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) )
139 115 adantl 
 |-  ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o )
140 139 a1i 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) )
141 138 140 jcad 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) -> ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) )
142 109 117 141 3orim123d 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) -> ( ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) ) )
143 fvex 
 |-  ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. _V
144 fvex 
 |-  ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) e. _V
145 143 144 brtp 
 |-  ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) <-> ( ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) = 2o ) ) )
146 142 15 145 3imtr4g 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( ( A |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) -> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
147 12 146 sylbid 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
148 147 imp 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
149 raleq 
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( A. y e. x ( A ` y ) = ( B ` y ) <-> A. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ( A ` y ) = ( B ` y ) ) )
150 fveq2 
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( A ` x ) = ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
151 fveq2 
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( B ` x ) = ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) )
152 150 151 breq12d 
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) )
153 149 152 anbi12d 
 |-  ( x = |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } -> ( ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> ( A. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ( A ` y ) = ( B ` y ) /\ ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) ) )
154 153 rspcev 
 |-  ( ( |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } e. On /\ ( A. y e. |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ( A ` y ) = ( B ` y ) /\ ( A ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( ( A |` X ) ` a ) =/= ( ( B |` X ) ` a ) } ) ) ) -> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
155 9 78 148 154 syl12anc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
156 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 ) ) ) )
157 156 3adant3 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
158 157 adantr 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
159 155 158 mpbird 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( A |` X )  A
160 159 ex 
 |-  ( ( A e. No /\ B e. No /\ X e. On ) -> ( ( A |` X )  A