Step |
Hyp |
Ref |
Expression |
1 |
|
sltso |
|- |
2 |
|
simp11 |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A A e. No ) |
3 |
|
sonr |
|- ( ( -. A |
4 |
1 2 3
|
sylancr |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A -. A |
5 |
|
simpl2r |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A A |
6 |
|
simpl2l |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A |` X ) = ( B |` X ) ) |
7 |
|
simpl11 |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A A e. No ) |
8 |
|
nofun |
|- ( A e. No -> Fun A ) |
9 |
|
funrel |
|- ( Fun A -> Rel A ) |
10 |
8 9
|
syl |
|- ( A e. No -> Rel A ) |
11 |
7 10
|
syl |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A Rel A ) |
12 |
|
simpl13 |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A X e. On ) |
13 |
|
simpr |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A ` X ) = (/) ) |
14 |
|
nolt02olem |
|- ( ( A e. No /\ X e. On /\ ( A ` X ) = (/) ) -> dom A C_ X ) |
15 |
7 12 13 14
|
syl3anc |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A dom A C_ X ) |
16 |
|
relssres |
|- ( ( Rel A /\ dom A C_ X ) -> ( A |` X ) = A ) |
17 |
11 15 16
|
syl2anc |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A |` X ) = A ) |
18 |
|
simpl12 |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A B e. No ) |
19 |
|
nofun |
|- ( B e. No -> Fun B ) |
20 |
|
funrel |
|- ( Fun B -> Rel B ) |
21 |
19 20
|
syl |
|- ( B e. No -> Rel B ) |
22 |
18 21
|
syl |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A Rel B ) |
23 |
|
simpl3 |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( B ` X ) = (/) ) |
24 |
|
nolt02olem |
|- ( ( B e. No /\ X e. On /\ ( B ` X ) = (/) ) -> dom B C_ X ) |
25 |
18 12 23 24
|
syl3anc |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A dom B C_ X ) |
26 |
|
relssres |
|- ( ( Rel B /\ dom B C_ X ) -> ( B |` X ) = B ) |
27 |
22 25 26
|
syl2anc |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( B |` X ) = B ) |
28 |
6 17 27
|
3eqtr3d |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A A = B ) |
29 |
5 28
|
breqtrrd |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A A |
30 |
4 29
|
mtand |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A -. ( A ` X ) = (/) ) |
31 |
|
simp2r |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A A |
32 |
|
simp12 |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A B e. No ) |
33 |
|
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 ) ) ) ) |
34 |
2 32 33
|
syl2anc |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) ) |
35 |
31 34
|
mpbid |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
36 |
|
ralinexa |
|- ( A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> -. E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
37 |
36
|
con2bii |
|- ( E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) <-> -. A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
38 |
35 37
|
sylib |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A -. A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
39 |
|
1n0 |
|- 1o =/= (/) |
40 |
39
|
neii |
|- -. 1o = (/) |
41 |
|
eqtr2 |
|- ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) -> 1o = (/) ) |
42 |
40 41
|
mto |
|- -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) |
43 |
|
df-2o |
|- 2o = suc 1o |
44 |
|
2on |
|- 2o e. On |
45 |
43 44
|
eqeltrri |
|- suc 1o e. On |
46 |
45
|
onordi |
|- Ord suc 1o |
47 |
|
1oex |
|- 1o e. _V |
48 |
47
|
sucid |
|- 1o e. suc 1o |
49 |
|
nordeq |
|- ( ( Ord suc 1o /\ 1o e. suc 1o ) -> suc 1o =/= 1o ) |
50 |
46 48 49
|
mp2an |
|- suc 1o =/= 1o |
51 |
43 50
|
eqnetri |
|- 2o =/= 1o |
52 |
51
|
nesymi |
|- -. 1o = 2o |
53 |
|
eqtr2 |
|- ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) -> 1o = 2o ) |
54 |
52 53
|
mto |
|- -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) |
55 |
|
2on0 |
|- 2o =/= (/) |
56 |
55
|
nesymi |
|- -. (/) = 2o |
57 |
|
eqtr2 |
|- ( ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) -> (/) = 2o ) |
58 |
56 57
|
mto |
|- -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) |
59 |
42 54 58
|
3pm3.2i |
|- ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) |
60 |
|
fvex |
|- ( ( A |` X ) ` x ) e. _V |
61 |
60 60
|
brtp |
|- ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) \/ ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) \/ ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) ) |
62 |
|
3oran |
|- ( ( ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) \/ ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) \/ ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) <-> -. ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) ) |
63 |
61 62
|
bitri |
|- ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> -. ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) ) |
64 |
63
|
con2bii |
|- ( ( -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = (/) ) /\ -. ( ( ( A |` X ) ` x ) = 1o /\ ( ( A |` X ) ` x ) = 2o ) /\ -. ( ( ( A |` X ) ` x ) = (/) /\ ( ( A |` X ) ` x ) = 2o ) ) <-> -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) ) |
65 |
59 64
|
mpbi |
|- -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) |
66 |
|
simpl2l |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A |` X ) = ( B |` X ) ) |
67 |
66
|
adantr |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A |` X ) = ( B |` X ) ) |
68 |
67
|
fveq1d |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( ( A |` X ) ` x ) = ( ( B |` X ) ` x ) ) |
69 |
68
|
breq2d |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A |` X ) ` x ) <-> ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) ) ) |
70 |
65 69
|
mtbii |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) ) |
71 |
|
fvres |
|- ( x e. X -> ( ( A |` X ) ` x ) = ( A ` x ) ) |
72 |
|
fvres |
|- ( x e. X -> ( ( B |` X ) ` x ) = ( B ` x ) ) |
73 |
71 72
|
breq12d |
|- ( x e. X -> ( ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) <-> ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
74 |
73
|
notbid |
|- ( x e. X -> ( -. ( ( A |` X ) ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( B |` X ) ` x ) <-> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
75 |
70 74
|
syl5ibcom |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( x e. X -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
76 |
51
|
neii |
|- -. 2o = 1o |
77 |
76
|
intnanr |
|- -. ( 2o = 1o /\ (/) = (/) ) |
78 |
56
|
intnan |
|- -. ( 2o = 1o /\ (/) = 2o ) |
79 |
56
|
intnan |
|- -. ( 2o = (/) /\ (/) = 2o ) |
80 |
77 78 79
|
3pm3.2i |
|- ( -. ( 2o = 1o /\ (/) = (/) ) /\ -. ( 2o = 1o /\ (/) = 2o ) /\ -. ( 2o = (/) /\ (/) = 2o ) ) |
81 |
|
2oex |
|- 2o e. _V |
82 |
|
0ex |
|- (/) e. _V |
83 |
81 82
|
brtp |
|- ( 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) <-> ( ( 2o = 1o /\ (/) = (/) ) \/ ( 2o = 1o /\ (/) = 2o ) \/ ( 2o = (/) /\ (/) = 2o ) ) ) |
84 |
|
3oran |
|- ( ( ( 2o = 1o /\ (/) = (/) ) \/ ( 2o = 1o /\ (/) = 2o ) \/ ( 2o = (/) /\ (/) = 2o ) ) <-> -. ( -. ( 2o = 1o /\ (/) = (/) ) /\ -. ( 2o = 1o /\ (/) = 2o ) /\ -. ( 2o = (/) /\ (/) = 2o ) ) ) |
85 |
83 84
|
bitri |
|- ( 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) <-> -. ( -. ( 2o = 1o /\ (/) = (/) ) /\ -. ( 2o = 1o /\ (/) = 2o ) /\ -. ( 2o = (/) /\ (/) = 2o ) ) ) |
86 |
85
|
con2bii |
|- ( ( -. ( 2o = 1o /\ (/) = (/) ) /\ -. ( 2o = 1o /\ (/) = 2o ) /\ -. ( 2o = (/) /\ (/) = 2o ) ) <-> -. 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) ) |
87 |
80 86
|
mpbi |
|- -. 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) |
88 |
|
simplr |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A ` X ) = 2o ) |
89 |
|
simpll3 |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( B ` X ) = (/) ) |
90 |
88 89
|
breq12d |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) <-> 2o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } (/) ) ) |
91 |
87 90
|
mtbiri |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A -. ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) |
92 |
|
fveq2 |
|- ( x = X -> ( A ` x ) = ( A ` X ) ) |
93 |
|
fveq2 |
|- ( x = X -> ( B ` x ) = ( B ` X ) ) |
94 |
92 93
|
breq12d |
|- ( x = X -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) ) |
95 |
94
|
notbid |
|- ( x = X -> ( -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) <-> -. ( A ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` X ) ) ) |
96 |
91 95
|
syl5ibrcom |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( x = X -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
97 |
|
fveq2 |
|- ( y = X -> ( A ` y ) = ( A ` X ) ) |
98 |
|
fveq2 |
|- ( y = X -> ( B ` y ) = ( B ` X ) ) |
99 |
97 98
|
eqeq12d |
|- ( y = X -> ( ( A ` y ) = ( B ` y ) <-> ( A ` X ) = ( B ` X ) ) ) |
100 |
99
|
rspccv |
|- ( A. y e. x ( A ` y ) = ( B ` y ) -> ( X e. x -> ( A ` X ) = ( B ` X ) ) ) |
101 |
100
|
ad2antll |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( X e. x -> ( A ` X ) = ( B ` X ) ) ) |
102 |
|
eqcom |
|- ( ( A ` X ) = ( B ` X ) <-> ( B ` X ) = ( A ` X ) ) |
103 |
101 102
|
syl6ib |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( X e. x -> ( B ` X ) = ( A ` X ) ) ) |
104 |
89 88
|
eqeq12d |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( ( B ` X ) = ( A ` X ) <-> (/) = 2o ) ) |
105 |
103 104
|
sylibd |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( X e. x -> (/) = 2o ) ) |
106 |
56 105
|
mtoi |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A -. X e. x ) |
107 |
|
simprl |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A x e. On ) |
108 |
|
simpl13 |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A X e. On ) |
109 |
108
|
adantr |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A X e. On ) |
110 |
|
ontri1 |
|- ( ( x e. On /\ X e. On ) -> ( x C_ X <-> -. X e. x ) ) |
111 |
|
onsseleq |
|- ( ( x e. On /\ X e. On ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) ) |
112 |
110 111
|
bitr3d |
|- ( ( x e. On /\ X e. On ) -> ( -. X e. x <-> ( x e. X \/ x = X ) ) ) |
113 |
107 109 112
|
syl2anc |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( -. X e. x <-> ( x e. X \/ x = X ) ) ) |
114 |
106 113
|
mpbid |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( x e. X \/ x = X ) ) |
115 |
75 96 114
|
mpjaod |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) |
116 |
115
|
expr |
|- ( ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
117 |
116
|
ralrimiva |
|- ( ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A A. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) -> -. ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) |
118 |
38 117
|
mtand |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A -. ( A ` X ) = 2o ) |
119 |
|
nofv |
|- ( A e. No -> ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) ) |
120 |
2 119
|
syl |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) ) |
121 |
|
3orcoma |
|- ( ( ( A ` X ) = (/) \/ ( A ` X ) = 1o \/ ( A ` X ) = 2o ) <-> ( ( A ` X ) = 1o \/ ( A ` X ) = (/) \/ ( A ` X ) = 2o ) ) |
122 |
120 121
|
sylib |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( ( A ` X ) = 1o \/ ( A ` X ) = (/) \/ ( A ` X ) = 2o ) ) |
123 |
30 118 122
|
ecase23d |
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ A ( A ` X ) = 1o ) |