Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
|- S = dom ( A CNF B ) |
2 |
|
cantnfs.a |
|- ( ph -> A e. On ) |
3 |
|
cantnfs.b |
|- ( ph -> B e. On ) |
4 |
|
oemapval.t |
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } |
5 |
|
oemapval.f |
|- ( ph -> F e. S ) |
6 |
|
oemapval.g |
|- ( ph -> G e. S ) |
7 |
|
oemapvali.r |
|- ( ph -> F T G ) |
8 |
|
oemapvali.x |
|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) } |
9 |
|
cantnflem1.o |
|- O = OrdIso ( _E , ( G supp (/) ) ) |
10 |
|
cantnflem1.h |
|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) ) |
11 |
|
ovex |
|- ( G supp (/) ) e. _V |
12 |
9
|
oion |
|- ( ( G supp (/) ) e. _V -> dom O e. On ) |
13 |
11 12
|
mp1i |
|- ( ph -> dom O e. On ) |
14 |
|
uniexg |
|- ( dom O e. On -> U. dom O e. _V ) |
15 |
|
sucidg |
|- ( U. dom O e. _V -> U. dom O e. suc U. dom O ) |
16 |
13 14 15
|
3syl |
|- ( ph -> U. dom O e. suc U. dom O ) |
17 |
1 2 3 4 5 6 7 8
|
cantnflem1a |
|- ( ph -> X e. ( G supp (/) ) ) |
18 |
|
n0i |
|- ( X e. ( G supp (/) ) -> -. ( G supp (/) ) = (/) ) |
19 |
17 18
|
syl |
|- ( ph -> -. ( G supp (/) ) = (/) ) |
20 |
|
ovexd |
|- ( ph -> ( G supp (/) ) e. _V ) |
21 |
1 2 3 9 6
|
cantnfcl |
|- ( ph -> ( _E We ( G supp (/) ) /\ dom O e. _om ) ) |
22 |
21
|
simpld |
|- ( ph -> _E We ( G supp (/) ) ) |
23 |
9
|
oien |
|- ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> dom O ~~ ( G supp (/) ) ) |
24 |
20 22 23
|
syl2anc |
|- ( ph -> dom O ~~ ( G supp (/) ) ) |
25 |
|
breq1 |
|- ( dom O = (/) -> ( dom O ~~ ( G supp (/) ) <-> (/) ~~ ( G supp (/) ) ) ) |
26 |
|
ensymb |
|- ( (/) ~~ ( G supp (/) ) <-> ( G supp (/) ) ~~ (/) ) |
27 |
|
en0 |
|- ( ( G supp (/) ) ~~ (/) <-> ( G supp (/) ) = (/) ) |
28 |
26 27
|
bitri |
|- ( (/) ~~ ( G supp (/) ) <-> ( G supp (/) ) = (/) ) |
29 |
25 28
|
bitrdi |
|- ( dom O = (/) -> ( dom O ~~ ( G supp (/) ) <-> ( G supp (/) ) = (/) ) ) |
30 |
24 29
|
syl5ibcom |
|- ( ph -> ( dom O = (/) -> ( G supp (/) ) = (/) ) ) |
31 |
19 30
|
mtod |
|- ( ph -> -. dom O = (/) ) |
32 |
21
|
simprd |
|- ( ph -> dom O e. _om ) |
33 |
|
nnlim |
|- ( dom O e. _om -> -. Lim dom O ) |
34 |
32 33
|
syl |
|- ( ph -> -. Lim dom O ) |
35 |
|
ioran |
|- ( -. ( dom O = (/) \/ Lim dom O ) <-> ( -. dom O = (/) /\ -. Lim dom O ) ) |
36 |
31 34 35
|
sylanbrc |
|- ( ph -> -. ( dom O = (/) \/ Lim dom O ) ) |
37 |
9
|
oicl |
|- Ord dom O |
38 |
|
unizlim |
|- ( Ord dom O -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) ) |
39 |
37 38
|
mp1i |
|- ( ph -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) ) |
40 |
36 39
|
mtbird |
|- ( ph -> -. dom O = U. dom O ) |
41 |
|
orduniorsuc |
|- ( Ord dom O -> ( dom O = U. dom O \/ dom O = suc U. dom O ) ) |
42 |
37 41
|
mp1i |
|- ( ph -> ( dom O = U. dom O \/ dom O = suc U. dom O ) ) |
43 |
42
|
ord |
|- ( ph -> ( -. dom O = U. dom O -> dom O = suc U. dom O ) ) |
44 |
40 43
|
mpd |
|- ( ph -> dom O = suc U. dom O ) |
45 |
16 44
|
eleqtrrd |
|- ( ph -> U. dom O e. dom O ) |
46 |
9
|
oiiso |
|- ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) ) |
47 |
20 22 46
|
syl2anc |
|- ( ph -> O Isom _E , _E ( dom O , ( G supp (/) ) ) ) |
48 |
|
isof1o |
|- ( O Isom _E , _E ( dom O , ( G supp (/) ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) ) |
49 |
47 48
|
syl |
|- ( ph -> O : dom O -1-1-onto-> ( G supp (/) ) ) |
50 |
|
f1ocnv |
|- ( O : dom O -1-1-onto-> ( G supp (/) ) -> `' O : ( G supp (/) ) -1-1-onto-> dom O ) |
51 |
|
f1of |
|- ( `' O : ( G supp (/) ) -1-1-onto-> dom O -> `' O : ( G supp (/) ) --> dom O ) |
52 |
49 50 51
|
3syl |
|- ( ph -> `' O : ( G supp (/) ) --> dom O ) |
53 |
52 17
|
ffvelrnd |
|- ( ph -> ( `' O ` X ) e. dom O ) |
54 |
|
elssuni |
|- ( ( `' O ` X ) e. dom O -> ( `' O ` X ) C_ U. dom O ) |
55 |
53 54
|
syl |
|- ( ph -> ( `' O ` X ) C_ U. dom O ) |
56 |
44 32
|
eqeltrrd |
|- ( ph -> suc U. dom O e. _om ) |
57 |
|
peano2b |
|- ( U. dom O e. _om <-> suc U. dom O e. _om ) |
58 |
56 57
|
sylibr |
|- ( ph -> U. dom O e. _om ) |
59 |
|
eleq1 |
|- ( y = U. dom O -> ( y e. dom O <-> U. dom O e. dom O ) ) |
60 |
|
sseq2 |
|- ( y = U. dom O -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ U. dom O ) ) |
61 |
59 60
|
anbi12d |
|- ( y = U. dom O -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) ) ) |
62 |
|
fveq2 |
|- ( y = U. dom O -> ( O ` y ) = ( O ` U. dom O ) ) |
63 |
62
|
sseq2d |
|- ( y = U. dom O -> ( x C_ ( O ` y ) <-> x C_ ( O ` U. dom O ) ) ) |
64 |
63
|
ifbid |
|- ( y = U. dom O -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) |
65 |
64
|
mpteq2dv |
|- ( y = U. dom O -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) |
66 |
65
|
fveq2d |
|- ( y = U. dom O -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) ) |
67 |
|
suceq |
|- ( y = U. dom O -> suc y = suc U. dom O ) |
68 |
67
|
fveq2d |
|- ( y = U. dom O -> ( H ` suc y ) = ( H ` suc U. dom O ) ) |
69 |
66 68
|
eleq12d |
|- ( y = U. dom O -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) |
70 |
61 69
|
imbi12d |
|- ( y = U. dom O -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) ) |
71 |
70
|
imbi2d |
|- ( y = U. dom O -> ( ( ph -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) ) <-> ( ph -> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) ) ) |
72 |
|
eleq1 |
|- ( y = (/) -> ( y e. dom O <-> (/) e. dom O ) ) |
73 |
|
sseq2 |
|- ( y = (/) -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ (/) ) ) |
74 |
72 73
|
anbi12d |
|- ( y = (/) -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) ) ) |
75 |
|
fveq2 |
|- ( y = (/) -> ( O ` y ) = ( O ` (/) ) ) |
76 |
75
|
sseq2d |
|- ( y = (/) -> ( x C_ ( O ` y ) <-> x C_ ( O ` (/) ) ) ) |
77 |
76
|
ifbid |
|- ( y = (/) -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) |
78 |
77
|
mpteq2dv |
|- ( y = (/) -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) |
79 |
78
|
fveq2d |
|- ( y = (/) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) ) |
80 |
|
suceq |
|- ( y = (/) -> suc y = suc (/) ) |
81 |
80
|
fveq2d |
|- ( y = (/) -> ( H ` suc y ) = ( H ` suc (/) ) ) |
82 |
79 81
|
eleq12d |
|- ( y = (/) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) ) |
83 |
74 82
|
imbi12d |
|- ( y = (/) -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) ) ) |
84 |
|
eleq1 |
|- ( y = u -> ( y e. dom O <-> u e. dom O ) ) |
85 |
|
sseq2 |
|- ( y = u -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ u ) ) |
86 |
84 85
|
anbi12d |
|- ( y = u -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( u e. dom O /\ ( `' O ` X ) C_ u ) ) ) |
87 |
|
fveq2 |
|- ( y = u -> ( O ` y ) = ( O ` u ) ) |
88 |
87
|
sseq2d |
|- ( y = u -> ( x C_ ( O ` y ) <-> x C_ ( O ` u ) ) ) |
89 |
88
|
ifbid |
|- ( y = u -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) |
90 |
89
|
mpteq2dv |
|- ( y = u -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) |
91 |
90
|
fveq2d |
|- ( y = u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) |
92 |
|
suceq |
|- ( y = u -> suc y = suc u ) |
93 |
92
|
fveq2d |
|- ( y = u -> ( H ` suc y ) = ( H ` suc u ) ) |
94 |
91 93
|
eleq12d |
|- ( y = u -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) ) |
95 |
86 94
|
imbi12d |
|- ( y = u -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) ) ) |
96 |
|
eleq1 |
|- ( y = suc u -> ( y e. dom O <-> suc u e. dom O ) ) |
97 |
|
sseq2 |
|- ( y = suc u -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ suc u ) ) |
98 |
96 97
|
anbi12d |
|- ( y = suc u -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) ) ) |
99 |
|
fveq2 |
|- ( y = suc u -> ( O ` y ) = ( O ` suc u ) ) |
100 |
99
|
sseq2d |
|- ( y = suc u -> ( x C_ ( O ` y ) <-> x C_ ( O ` suc u ) ) ) |
101 |
100
|
ifbid |
|- ( y = suc u -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) |
102 |
101
|
mpteq2dv |
|- ( y = suc u -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) |
103 |
102
|
fveq2d |
|- ( y = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) ) |
104 |
|
suceq |
|- ( y = suc u -> suc y = suc suc u ) |
105 |
104
|
fveq2d |
|- ( y = suc u -> ( H ` suc y ) = ( H ` suc suc u ) ) |
106 |
103 105
|
eleq12d |
|- ( y = suc u -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) |
107 |
98 106
|
imbi12d |
|- ( y = suc u -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) |
108 |
|
f1ocnvfv2 |
|- ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ X e. ( G supp (/) ) ) -> ( O ` ( `' O ` X ) ) = X ) |
109 |
49 17 108
|
syl2anc |
|- ( ph -> ( O ` ( `' O ` X ) ) = X ) |
110 |
109
|
sseq2d |
|- ( ph -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ X ) ) |
111 |
110
|
ifbid |
|- ( ph -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ X , ( F ` x ) , (/) ) ) |
112 |
111
|
mpteq2dv |
|- ( ph -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) |
113 |
112
|
fveq2d |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) ) |
114 |
1 2 3 4 5 6 7 8 9 10
|
cantnflem1d |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) ) |
115 |
113 114
|
eqeltrd |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) ) |
116 |
|
ss0 |
|- ( ( `' O ` X ) C_ (/) -> ( `' O ` X ) = (/) ) |
117 |
116
|
fveq2d |
|- ( ( `' O ` X ) C_ (/) -> ( O ` ( `' O ` X ) ) = ( O ` (/) ) ) |
118 |
117
|
sseq2d |
|- ( ( `' O ` X ) C_ (/) -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ ( O ` (/) ) ) ) |
119 |
118
|
ifbid |
|- ( ( `' O ` X ) C_ (/) -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) |
120 |
119
|
mpteq2dv |
|- ( ( `' O ` X ) C_ (/) -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) |
121 |
120
|
fveq2d |
|- ( ( `' O ` X ) C_ (/) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) ) |
122 |
|
suceq |
|- ( ( `' O ` X ) = (/) -> suc ( `' O ` X ) = suc (/) ) |
123 |
116 122
|
syl |
|- ( ( `' O ` X ) C_ (/) -> suc ( `' O ` X ) = suc (/) ) |
124 |
123
|
fveq2d |
|- ( ( `' O ` X ) C_ (/) -> ( H ` suc ( `' O ` X ) ) = ( H ` suc (/) ) ) |
125 |
121 124
|
eleq12d |
|- ( ( `' O ` X ) C_ (/) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) ) |
126 |
125
|
adantl |
|- ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) ) |
127 |
115 126
|
syl5ibcom |
|- ( ph -> ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) ) |
128 |
|
ordelon |
|- ( ( Ord dom O /\ ( `' O ` X ) e. dom O ) -> ( `' O ` X ) e. On ) |
129 |
37 53 128
|
sylancr |
|- ( ph -> ( `' O ` X ) e. On ) |
130 |
37
|
a1i |
|- ( ph -> Ord dom O ) |
131 |
|
ordelon |
|- ( ( Ord dom O /\ suc u e. dom O ) -> suc u e. On ) |
132 |
130 131
|
sylan |
|- ( ( ph /\ suc u e. dom O ) -> suc u e. On ) |
133 |
|
onsseleq |
|- ( ( ( `' O ` X ) e. On /\ suc u e. On ) -> ( ( `' O ` X ) C_ suc u <-> ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) ) ) |
134 |
129 132 133
|
syl2an2r |
|- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ suc u <-> ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) ) ) |
135 |
|
sucelon |
|- ( u e. On <-> suc u e. On ) |
136 |
132 135
|
sylibr |
|- ( ( ph /\ suc u e. dom O ) -> u e. On ) |
137 |
|
eloni |
|- ( u e. On -> Ord u ) |
138 |
136 137
|
syl |
|- ( ( ph /\ suc u e. dom O ) -> Ord u ) |
139 |
|
ordsssuc |
|- ( ( ( `' O ` X ) e. On /\ Ord u ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) ) |
140 |
129 138 139
|
syl2an2r |
|- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) ) |
141 |
|
ordtr |
|- ( Ord dom O -> Tr dom O ) |
142 |
37 141
|
mp1i |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Tr dom O ) |
143 |
|
simprl |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. dom O ) |
144 |
|
trsuc |
|- ( ( Tr dom O /\ suc u e. dom O ) -> u e. dom O ) |
145 |
142 143 144
|
syl2anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> u e. dom O ) |
146 |
|
simprr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) C_ u ) |
147 |
145 146
|
jca |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. dom O /\ ( `' O ` X ) C_ u ) ) |
148 |
3
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> B e. On ) |
149 |
|
oecl |
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On ) |
150 |
2 148 149
|
syl2an2r |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A ^o B ) e. On ) |
151 |
2
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A e. On ) |
152 |
1 151 148
|
cantnff |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A CNF B ) : S --> ( A ^o B ) ) |
153 |
1 2 3
|
cantnfs |
|- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) ) |
154 |
5 153
|
mpbid |
|- ( ph -> ( F : B --> A /\ F finSupp (/) ) ) |
155 |
154
|
simpld |
|- ( ph -> F : B --> A ) |
156 |
155
|
ffvelrnda |
|- ( ( ph /\ x e. B ) -> ( F ` x ) e. A ) |
157 |
1 2 3
|
cantnfs |
|- ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) ) |
158 |
6 157
|
mpbid |
|- ( ph -> ( G : B --> A /\ G finSupp (/) ) ) |
159 |
158
|
simpld |
|- ( ph -> G : B --> A ) |
160 |
1 2 3 4 5 6 7 8
|
oemapvali |
|- ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) ) |
161 |
160
|
simp1d |
|- ( ph -> X e. B ) |
162 |
159 161
|
ffvelrnd |
|- ( ph -> ( G ` X ) e. A ) |
163 |
162
|
ne0d |
|- ( ph -> A =/= (/) ) |
164 |
|
on0eln0 |
|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) ) |
165 |
2 164
|
syl |
|- ( ph -> ( (/) e. A <-> A =/= (/) ) ) |
166 |
163 165
|
mpbird |
|- ( ph -> (/) e. A ) |
167 |
166
|
adantr |
|- ( ( ph /\ x e. B ) -> (/) e. A ) |
168 |
156 167
|
ifcld |
|- ( ( ph /\ x e. B ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. A ) |
169 |
168
|
fmpttd |
|- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) : B --> A ) |
170 |
3
|
mptexd |
|- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. _V ) |
171 |
|
funmpt |
|- Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) |
172 |
171
|
a1i |
|- ( ph -> Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) |
173 |
154
|
simprd |
|- ( ph -> F finSupp (/) ) |
174 |
|
ssidd |
|- ( ph -> ( F supp (/) ) C_ ( F supp (/) ) ) |
175 |
|
0ex |
|- (/) e. _V |
176 |
175
|
a1i |
|- ( ph -> (/) e. _V ) |
177 |
155 174 3 176
|
suppssr |
|- ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> ( F ` x ) = (/) ) |
178 |
177
|
ifeq1d |
|- ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , (/) , (/) ) ) |
179 |
|
ifid |
|- if ( x C_ ( O ` u ) , (/) , (/) ) = (/) |
180 |
178 179
|
eqtrdi |
|- ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) ) |
181 |
180 3
|
suppss2 |
|- ( ph -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( F supp (/) ) ) |
182 |
|
fsuppsssupp |
|- ( ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. _V /\ Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) /\ ( F finSupp (/) /\ ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( F supp (/) ) ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) finSupp (/) ) |
183 |
170 172 173 181 182
|
syl22anc |
|- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) finSupp (/) ) |
184 |
1 2 3
|
cantnfs |
|- ( ph -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S <-> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) : B --> A /\ ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) finSupp (/) ) ) ) |
185 |
169 183 184
|
mpbir2and |
|- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S ) |
186 |
185
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S ) |
187 |
152 186
|
ffvelrnd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( A ^o B ) ) |
188 |
|
onelon |
|- ( ( ( A ^o B ) e. On /\ ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( A ^o B ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On ) |
189 |
150 187 188
|
syl2anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On ) |
190 |
32
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> dom O e. _om ) |
191 |
|
elnn |
|- ( ( suc u e. dom O /\ dom O e. _om ) -> suc u e. _om ) |
192 |
143 190 191
|
syl2anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. _om ) |
193 |
10
|
cantnfvalf |
|- H : _om --> On |
194 |
193
|
ffvelrni |
|- ( suc u e. _om -> ( H ` suc u ) e. On ) |
195 |
192 194
|
syl |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( H ` suc u ) e. On ) |
196 |
|
suppssdm |
|- ( G supp (/) ) C_ dom G |
197 |
196 159
|
fssdm |
|- ( ph -> ( G supp (/) ) C_ B ) |
198 |
197
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( G supp (/) ) C_ B ) |
199 |
9
|
oif |
|- O : dom O --> ( G supp (/) ) |
200 |
199
|
ffvelrni |
|- ( suc u e. dom O -> ( O ` suc u ) e. ( G supp (/) ) ) |
201 |
143 200
|
syl |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. ( G supp (/) ) ) |
202 |
198 201
|
sseldd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. B ) |
203 |
|
onelon |
|- ( ( B e. On /\ ( O ` suc u ) e. B ) -> ( O ` suc u ) e. On ) |
204 |
3 202 203
|
syl2an2r |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. On ) |
205 |
|
oecl |
|- ( ( A e. On /\ ( O ` suc u ) e. On ) -> ( A ^o ( O ` suc u ) ) e. On ) |
206 |
2 204 205
|
syl2an2r |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A ^o ( O ` suc u ) ) e. On ) |
207 |
155
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> F : B --> A ) |
208 |
207 202
|
ffvelrnd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) e. A ) |
209 |
|
onelon |
|- ( ( A e. On /\ ( F ` ( O ` suc u ) ) e. A ) -> ( F ` ( O ` suc u ) ) e. On ) |
210 |
2 208 209
|
syl2an2r |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) e. On ) |
211 |
|
omcl |
|- ( ( ( A ^o ( O ` suc u ) ) e. On /\ ( F ` ( O ` suc u ) ) e. On ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On ) |
212 |
206 210 211
|
syl2anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On ) |
213 |
|
oaord |
|- ( ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On /\ ( H ` suc u ) e. On /\ ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) <-> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) e. ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) ) |
214 |
189 195 212 213
|
syl3anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) <-> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) e. ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) ) |
215 |
|
ifeq1 |
|- ( ( F ` x ) = (/) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , (/) , (/) ) ) |
216 |
|
ifid |
|- if ( x C_ ( O ` suc u ) , (/) , (/) ) = (/) |
217 |
215 216
|
eqtrdi |
|- ( ( F ` x ) = (/) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = (/) ) |
218 |
|
ifeq1 |
|- ( ( F ` x ) = (/) -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , (/) , (/) ) ) |
219 |
|
ifid |
|- if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , (/) , (/) ) = (/) |
220 |
218 219
|
eqtrdi |
|- ( ( F ` x ) = (/) -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = (/) ) |
221 |
217 220
|
eqeq12d |
|- ( ( F ` x ) = (/) -> ( if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) <-> (/) = (/) ) ) |
222 |
|
onss |
|- ( B e. On -> B C_ On ) |
223 |
3 222
|
syl |
|- ( ph -> B C_ On ) |
224 |
223
|
sselda |
|- ( ( ph /\ x e. B ) -> x e. On ) |
225 |
224
|
adantlr |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> x e. On ) |
226 |
204
|
adantr |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( O ` suc u ) e. On ) |
227 |
|
onsseleq |
|- ( ( x e. On /\ ( O ` suc u ) e. On ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) ) |
228 |
225 226 227
|
syl2anc |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) ) |
229 |
228
|
adantr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) ) |
230 |
199
|
ffvelrni |
|- ( u e. dom O -> ( O ` u ) e. ( G supp (/) ) ) |
231 |
145 230
|
syl |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( G supp (/) ) ) |
232 |
198 231
|
sseldd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. B ) |
233 |
|
onelon |
|- ( ( B e. On /\ ( O ` u ) e. B ) -> ( O ` u ) e. On ) |
234 |
3 232 233
|
syl2an2r |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. On ) |
235 |
234
|
ad2antrr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( O ` u ) e. On ) |
236 |
|
onsssuc |
|- ( ( x e. On /\ ( O ` u ) e. On ) -> ( x C_ ( O ` u ) <-> x e. suc ( O ` u ) ) ) |
237 |
225 235 236
|
syl2an2r |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> x e. suc ( O ` u ) ) ) |
238 |
|
vex |
|- u e. _V |
239 |
238
|
sucid |
|- u e. suc u |
240 |
47
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) ) |
241 |
|
isorel |
|- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( u e. dom O /\ suc u e. dom O ) ) -> ( u _E suc u <-> ( O ` u ) _E ( O ` suc u ) ) ) |
242 |
240 145 143 241
|
syl12anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u _E suc u <-> ( O ` u ) _E ( O ` suc u ) ) ) |
243 |
238
|
sucex |
|- suc u e. _V |
244 |
243
|
epeli |
|- ( u _E suc u <-> u e. suc u ) |
245 |
|
fvex |
|- ( O ` suc u ) e. _V |
246 |
245
|
epeli |
|- ( ( O ` u ) _E ( O ` suc u ) <-> ( O ` u ) e. ( O ` suc u ) ) |
247 |
242 244 246
|
3bitr3g |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. suc u <-> ( O ` u ) e. ( O ` suc u ) ) ) |
248 |
239 247
|
mpbii |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( O ` suc u ) ) |
249 |
|
eloni |
|- ( ( O ` suc u ) e. On -> Ord ( O ` suc u ) ) |
250 |
204 249
|
syl |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Ord ( O ` suc u ) ) |
251 |
|
ordelsuc |
|- ( ( ( O ` u ) e. On /\ Ord ( O ` suc u ) ) -> ( ( O ` u ) e. ( O ` suc u ) <-> suc ( O ` u ) C_ ( O ` suc u ) ) ) |
252 |
234 250 251
|
syl2anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( O ` u ) e. ( O ` suc u ) <-> suc ( O ` u ) C_ ( O ` suc u ) ) ) |
253 |
248 252
|
mpbid |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc ( O ` u ) C_ ( O ` suc u ) ) |
254 |
253
|
ad2antrr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> suc ( O ` u ) C_ ( O ` suc u ) ) |
255 |
254
|
sseld |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. suc ( O ` u ) -> x e. ( O ` suc u ) ) ) |
256 |
237 255
|
sylbid |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) -> x e. ( O ` suc u ) ) ) |
257 |
|
simprr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. x ) |
258 |
240
|
ad2antrr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) ) |
259 |
258 48
|
syl |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) ) |
260 |
1 2 3 4 5 6 7 8 9
|
cantnflem1c |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. ( G supp (/) ) ) |
261 |
|
f1ocnvfv2 |
|- ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ x e. ( G supp (/) ) ) -> ( O ` ( `' O ` x ) ) = x ) |
262 |
259 260 261
|
syl2anc |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` ( `' O ` x ) ) = x ) |
263 |
257 262
|
eleqtrrd |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. ( O ` ( `' O ` x ) ) ) |
264 |
145
|
ad2antrr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> u e. dom O ) |
265 |
259 50 51
|
3syl |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> `' O : ( G supp (/) ) --> dom O ) |
266 |
265 260
|
ffvelrnd |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( `' O ` x ) e. dom O ) |
267 |
|
isorel |
|- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( u e. dom O /\ ( `' O ` x ) e. dom O ) ) -> ( u _E ( `' O ` x ) <-> ( O ` u ) _E ( O ` ( `' O ` x ) ) ) ) |
268 |
258 264 266 267
|
syl12anc |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u _E ( `' O ` x ) <-> ( O ` u ) _E ( O ` ( `' O ` x ) ) ) ) |
269 |
|
fvex |
|- ( `' O ` x ) e. _V |
270 |
269
|
epeli |
|- ( u _E ( `' O ` x ) <-> u e. ( `' O ` x ) ) |
271 |
|
fvex |
|- ( O ` ( `' O ` x ) ) e. _V |
272 |
271
|
epeli |
|- ( ( O ` u ) _E ( O ` ( `' O ` x ) ) <-> ( O ` u ) e. ( O ` ( `' O ` x ) ) ) |
273 |
268 270 272
|
3bitr3g |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u e. ( `' O ` x ) <-> ( O ` u ) e. ( O ` ( `' O ` x ) ) ) ) |
274 |
263 273
|
mpbird |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> u e. ( `' O ` x ) ) |
275 |
|
ordelon |
|- ( ( Ord dom O /\ ( `' O ` x ) e. dom O ) -> ( `' O ` x ) e. On ) |
276 |
37 266 275
|
sylancr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( `' O ` x ) e. On ) |
277 |
|
eloni |
|- ( ( `' O ` x ) e. On -> Ord ( `' O ` x ) ) |
278 |
276 277
|
syl |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> Ord ( `' O ` x ) ) |
279 |
|
ordelsuc |
|- ( ( u e. ( `' O ` x ) /\ Ord ( `' O ` x ) ) -> ( u e. ( `' O ` x ) <-> suc u C_ ( `' O ` x ) ) ) |
280 |
274 278 279
|
syl2anc |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u e. ( `' O ` x ) <-> suc u C_ ( `' O ` x ) ) ) |
281 |
274 280
|
mpbid |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u C_ ( `' O ` x ) ) |
282 |
143
|
ad2antrr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u e. dom O ) |
283 |
37 282 131
|
sylancr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u e. On ) |
284 |
|
ontri1 |
|- ( ( suc u e. On /\ ( `' O ` x ) e. On ) -> ( suc u C_ ( `' O ` x ) <-> -. ( `' O ` x ) e. suc u ) ) |
285 |
283 276 284
|
syl2anc |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( suc u C_ ( `' O ` x ) <-> -. ( `' O ` x ) e. suc u ) ) |
286 |
281 285
|
mpbid |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> -. ( `' O ` x ) e. suc u ) |
287 |
|
isorel |
|- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( ( `' O ` x ) e. dom O /\ suc u e. dom O ) ) -> ( ( `' O ` x ) _E suc u <-> ( O ` ( `' O ` x ) ) _E ( O ` suc u ) ) ) |
288 |
258 266 282 287
|
syl12anc |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) _E suc u <-> ( O ` ( `' O ` x ) ) _E ( O ` suc u ) ) ) |
289 |
243
|
epeli |
|- ( ( `' O ` x ) _E suc u <-> ( `' O ` x ) e. suc u ) |
290 |
245
|
epeli |
|- ( ( O ` ( `' O ` x ) ) _E ( O ` suc u ) <-> ( O ` ( `' O ` x ) ) e. ( O ` suc u ) ) |
291 |
288 289 290
|
3bitr3g |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) e. suc u <-> ( O ` ( `' O ` x ) ) e. ( O ` suc u ) ) ) |
292 |
262
|
eleq1d |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( O ` ( `' O ` x ) ) e. ( O ` suc u ) <-> x e. ( O ` suc u ) ) ) |
293 |
291 292
|
bitrd |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) e. suc u <-> x e. ( O ` suc u ) ) ) |
294 |
286 293
|
mtbid |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> -. x e. ( O ` suc u ) ) |
295 |
294
|
expr |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( ( O ` u ) e. x -> -. x e. ( O ` suc u ) ) ) |
296 |
295
|
con2d |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. ( O ` suc u ) -> -. ( O ` u ) e. x ) ) |
297 |
|
ontri1 |
|- ( ( x e. On /\ ( O ` u ) e. On ) -> ( x C_ ( O ` u ) <-> -. ( O ` u ) e. x ) ) |
298 |
225 235 297
|
syl2an2r |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> -. ( O ` u ) e. x ) ) |
299 |
296 298
|
sylibrd |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. ( O ` suc u ) -> x C_ ( O ` u ) ) ) |
300 |
256 299
|
impbid |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> x e. ( O ` suc u ) ) ) |
301 |
300
|
orbi1d |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) ) |
302 |
229 301
|
bitr4d |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) ) ) |
303 |
|
orcom |
|- ( ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) <-> ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) ) |
304 |
302 303
|
bitrdi |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) ) ) |
305 |
304
|
ifbid |
|- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) |
306 |
|
eqidd |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> (/) = (/) ) |
307 |
221 305 306
|
pm2.61ne |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) |
308 |
307
|
mpteq2dva |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) |
309 |
308
|
fveq2d |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) ) |
310 |
|
fvex |
|- ( F ` x ) e. _V |
311 |
310 175
|
ifex |
|- if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V |
312 |
311
|
a1i |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V ) |
313 |
312
|
ralrimivw |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A. x e. B if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V ) |
314 |
|
eqid |
|- ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) |
315 |
314
|
fnmpt |
|- ( A. x e. B if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B ) |
316 |
313 315
|
syl |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B ) |
317 |
175
|
a1i |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> (/) e. _V ) |
318 |
|
suppvalfn |
|- ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B /\ B e. On /\ (/) e. _V ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { y e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) } ) |
319 |
|
nfcv |
|- F/_ y B |
320 |
|
nfcv |
|- F/_ x B |
321 |
|
nffvmpt1 |
|- F/_ x ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) |
322 |
|
nfcv |
|- F/_ x (/) |
323 |
321 322
|
nfne |
|- F/ x ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) |
324 |
|
nfv |
|- F/ y ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) |
325 |
|
fveq2 |
|- ( y = x -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) = ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) ) |
326 |
325
|
neeq1d |
|- ( y = x -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) <-> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) ) ) |
327 |
319 320 323 324 326
|
cbvrabw |
|- { y e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) } = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } |
328 |
318 327
|
eqtrdi |
|- ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B /\ B e. On /\ (/) e. _V ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } ) |
329 |
316 148 317 328
|
syl3anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } ) |
330 |
|
eqidd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) |
331 |
311
|
a1i |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V ) |
332 |
330 331
|
fvmpt2d |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) = if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) |
333 |
332
|
neeq1d |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) ) |
334 |
331
|
biantrurd |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) <-> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) ) ) |
335 |
|
dif1o |
|- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) <-> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) ) |
336 |
334 335
|
bitr4di |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) ) |
337 |
333 336
|
bitrd |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) ) |
338 |
337
|
rabbidva |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } = { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } ) |
339 |
329 338
|
eqtrd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } ) |
340 |
311 335
|
mpbiran |
|- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) |
341 |
|
ifeq1 |
|- ( ( F ` x ) = (/) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , (/) , (/) ) ) |
342 |
341 179
|
eqtrdi |
|- ( ( F ` x ) = (/) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) ) |
343 |
342
|
necon3i |
|- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> ( F ` x ) =/= (/) ) |
344 |
|
iffalse |
|- ( -. x C_ ( O ` u ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) ) |
345 |
344
|
necon1ai |
|- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> x C_ ( O ` u ) ) |
346 |
343 345
|
jca |
|- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> ( ( F ` x ) =/= (/) /\ x C_ ( O ` u ) ) ) |
347 |
256
|
expimpd |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( F ` x ) =/= (/) /\ x C_ ( O ` u ) ) -> x e. ( O ` suc u ) ) ) |
348 |
346 347
|
syl5 |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> x e. ( O ` suc u ) ) ) |
349 |
340 348
|
syl5bi |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) -> x e. ( O ` suc u ) ) ) |
350 |
349
|
3impia |
|- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) -> x e. ( O ` suc u ) ) |
351 |
350
|
rabssdv |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } C_ ( O ` suc u ) ) |
352 |
339 351
|
eqsstrd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( O ` suc u ) ) |
353 |
|
eqeq1 |
|- ( x = y -> ( x = ( O ` suc u ) <-> y = ( O ` suc u ) ) ) |
354 |
|
sseq1 |
|- ( x = y -> ( x C_ ( O ` u ) <-> y C_ ( O ` u ) ) ) |
355 |
353 354
|
orbi12d |
|- ( x = y -> ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) <-> ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) ) ) |
356 |
|
fveq2 |
|- ( x = y -> ( F ` x ) = ( F ` y ) ) |
357 |
355 356
|
ifbieq1d |
|- ( x = y -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) ) |
358 |
357
|
cbvmptv |
|- ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) = ( y e. B |-> if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) ) |
359 |
|
fveq2 |
|- ( y = ( O ` suc u ) -> ( F ` y ) = ( F ` ( O ` suc u ) ) ) |
360 |
359
|
adantl |
|- ( ( y e. B /\ y = ( O ` suc u ) ) -> ( F ` y ) = ( F ` ( O ` suc u ) ) ) |
361 |
360
|
ifeq1da |
|- ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) ) |
362 |
354 356
|
ifbieq1d |
|- ( x = y -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) ) |
363 |
|
fvex |
|- ( F ` y ) e. _V |
364 |
363 175
|
ifex |
|- if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) e. _V |
365 |
362 314 364
|
fvmpt |
|- ( y e. B -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) = if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) ) |
366 |
365
|
ifeq2d |
|- ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( y = ( O ` suc u ) , ( F ` y ) , if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) ) ) |
367 |
|
ifor |
|- if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) = if ( y = ( O ` suc u ) , ( F ` y ) , if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) ) |
368 |
366 367
|
eqtr4di |
|- ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) ) |
369 |
361 368
|
eqtr3d |
|- ( y e. B -> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) ) |
370 |
369
|
mpteq2ia |
|- ( y e. B |-> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) ) = ( y e. B |-> if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) ) |
371 |
358 370
|
eqtr4i |
|- ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) = ( y e. B |-> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) ) |
372 |
1 151 148 186 202 208 352 371
|
cantnfp1 |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) e. S /\ ( ( A CNF B ) ` ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) ) ) |
373 |
372
|
simprd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) ) |
374 |
309 373
|
eqtrd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) ) |
375 |
1 2 3 9 6 10
|
cantnfsuc |
|- ( ( ph /\ suc u e. _om ) -> ( H ` suc suc u ) = ( ( ( A ^o ( O ` suc u ) ) .o ( G ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) |
376 |
192 375
|
syldan |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( H ` suc suc u ) = ( ( ( A ^o ( O ` suc u ) ) .o ( G ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) |
377 |
160
|
simp3d |
|- ( ph -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) |
378 |
377
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) |
379 |
109
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` ( `' O ` X ) ) = X ) |
380 |
136
|
adantrr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> u e. On ) |
381 |
|
onsssuc |
|- ( ( ( `' O ` X ) e. On /\ u e. On ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) ) |
382 |
129 380 381
|
syl2an2r |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) ) |
383 |
146 382
|
mpbid |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) e. suc u ) |
384 |
53
|
adantr |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) e. dom O ) |
385 |
|
isorel |
|- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( ( `' O ` X ) e. dom O /\ suc u e. dom O ) ) -> ( ( `' O ` X ) _E suc u <-> ( O ` ( `' O ` X ) ) _E ( O ` suc u ) ) ) |
386 |
240 384 143 385
|
syl12anc |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( `' O ` X ) _E suc u <-> ( O ` ( `' O ` X ) ) _E ( O ` suc u ) ) ) |
387 |
243
|
epeli |
|- ( ( `' O ` X ) _E suc u <-> ( `' O ` X ) e. suc u ) |
388 |
245
|
epeli |
|- ( ( O ` ( `' O ` X ) ) _E ( O ` suc u ) <-> ( O ` ( `' O ` X ) ) e. ( O ` suc u ) ) |
389 |
386 387 388
|
3bitr3g |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( `' O ` X ) e. suc u <-> ( O ` ( `' O ` X ) ) e. ( O ` suc u ) ) ) |
390 |
383 389
|
mpbid |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` ( `' O ` X ) ) e. ( O ` suc u ) ) |
391 |
379 390
|
eqeltrrd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> X e. ( O ` suc u ) ) |
392 |
|
eleq2 |
|- ( w = ( O ` suc u ) -> ( X e. w <-> X e. ( O ` suc u ) ) ) |
393 |
|
fveq2 |
|- ( w = ( O ` suc u ) -> ( F ` w ) = ( F ` ( O ` suc u ) ) ) |
394 |
|
fveq2 |
|- ( w = ( O ` suc u ) -> ( G ` w ) = ( G ` ( O ` suc u ) ) ) |
395 |
393 394
|
eqeq12d |
|- ( w = ( O ` suc u ) -> ( ( F ` w ) = ( G ` w ) <-> ( F ` ( O ` suc u ) ) = ( G ` ( O ` suc u ) ) ) ) |
396 |
392 395
|
imbi12d |
|- ( w = ( O ` suc u ) -> ( ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> ( X e. ( O ` suc u ) -> ( F ` ( O ` suc u ) ) = ( G ` ( O ` suc u ) ) ) ) ) |
397 |
396
|
rspcv |
|- ( ( O ` suc u ) e. B -> ( A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) -> ( X e. ( O ` suc u ) -> ( F ` ( O ` suc u ) ) = ( G ` ( O ` suc u ) ) ) ) ) |
398 |
202 378 391 397
|
syl3c |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) = ( G ` ( O ` suc u ) ) ) |
399 |
398
|
oveq2d |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) = ( ( A ^o ( O ` suc u ) ) .o ( G ` ( O ` suc u ) ) ) ) |
400 |
399
|
oveq1d |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( G ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) |
401 |
376 400
|
eqtr4d |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( H ` suc suc u ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) |
402 |
374 401
|
eleq12d |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) <-> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) e. ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) ) |
403 |
214 402
|
bitr4d |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) |
404 |
403
|
biimpd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) |
405 |
147 404
|
embantd |
|- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) |
406 |
405
|
expr |
|- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ u -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) |
407 |
140 406
|
sylbird |
|- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) e. suc u -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) |
408 |
|
fveq2 |
|- ( ( `' O ` X ) = suc u -> ( O ` ( `' O ` X ) ) = ( O ` suc u ) ) |
409 |
408
|
sseq2d |
|- ( ( `' O ` X ) = suc u -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ ( O ` suc u ) ) ) |
410 |
409
|
ifbid |
|- ( ( `' O ` X ) = suc u -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) |
411 |
410
|
mpteq2dv |
|- ( ( `' O ` X ) = suc u -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) |
412 |
411
|
fveq2d |
|- ( ( `' O ` X ) = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) ) |
413 |
|
suceq |
|- ( ( `' O ` X ) = suc u -> suc ( `' O ` X ) = suc suc u ) |
414 |
413
|
fveq2d |
|- ( ( `' O ` X ) = suc u -> ( H ` suc ( `' O ` X ) ) = ( H ` suc suc u ) ) |
415 |
412 414
|
eleq12d |
|- ( ( `' O ` X ) = suc u -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) |
416 |
115 415
|
syl5ibcom |
|- ( ph -> ( ( `' O ` X ) = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) |
417 |
416
|
adantr |
|- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) |
418 |
417
|
a1dd |
|- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) = suc u -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) |
419 |
407 418
|
jaod |
|- ( ( ph /\ suc u e. dom O ) -> ( ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) |
420 |
134 419
|
sylbid |
|- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ suc u -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) |
421 |
420
|
expimpd |
|- ( ph -> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) |
422 |
421
|
com23 |
|- ( ph -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) |
423 |
422
|
a1i |
|- ( u e. _om -> ( ph -> ( ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) -> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) ) ) |
424 |
83 95 107 127 423
|
finds2 |
|- ( y e. _om -> ( ph -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) ) ) |
425 |
71 424
|
vtoclga |
|- ( U. dom O e. _om -> ( ph -> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) ) |
426 |
58 425
|
mpcom |
|- ( ph -> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) |
427 |
45 55 426
|
mp2and |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) |
428 |
155
|
feqmptd |
|- ( ph -> F = ( x e. B |-> ( F ` x ) ) ) |
429 |
|
eqeq2 |
|- ( ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) -> ( ( F ` x ) = ( F ` x ) <-> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) |
430 |
|
eqeq2 |
|- ( (/) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) -> ( ( F ` x ) = (/) <-> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) |
431 |
|
eqidd |
|- ( ( ( ph /\ x e. B ) /\ x C_ ( O ` U. dom O ) ) -> ( F ` x ) = ( F ` x ) ) |
432 |
199
|
ffvelrni |
|- ( U. dom O e. dom O -> ( O ` U. dom O ) e. ( G supp (/) ) ) |
433 |
45 432
|
syl |
|- ( ph -> ( O ` U. dom O ) e. ( G supp (/) ) ) |
434 |
197 433
|
sseldd |
|- ( ph -> ( O ` U. dom O ) e. B ) |
435 |
|
onelon |
|- ( ( B e. On /\ ( O ` U. dom O ) e. B ) -> ( O ` U. dom O ) e. On ) |
436 |
3 434 435
|
syl2anc |
|- ( ph -> ( O ` U. dom O ) e. On ) |
437 |
436
|
adantr |
|- ( ( ph /\ x e. B ) -> ( O ` U. dom O ) e. On ) |
438 |
|
ontri1 |
|- ( ( x e. On /\ ( O ` U. dom O ) e. On ) -> ( x C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. x ) ) |
439 |
224 437 438
|
syl2anc |
|- ( ( ph /\ x e. B ) -> ( x C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. x ) ) |
440 |
439
|
con2bid |
|- ( ( ph /\ x e. B ) -> ( ( O ` U. dom O ) e. x <-> -. x C_ ( O ` U. dom O ) ) ) |
441 |
|
simprl |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. B ) |
442 |
377
|
adantr |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) |
443 |
|
eloni |
|- ( ( `' O ` X ) e. On -> Ord ( `' O ` X ) ) |
444 |
129 443
|
syl |
|- ( ph -> Ord ( `' O ` X ) ) |
445 |
|
orduni |
|- ( Ord dom O -> Ord U. dom O ) |
446 |
37 445
|
ax-mp |
|- Ord U. dom O |
447 |
|
ordtri1 |
|- ( ( Ord ( `' O ` X ) /\ Ord U. dom O ) -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) ) |
448 |
444 446 447
|
sylancl |
|- ( ph -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) ) |
449 |
55 448
|
mpbid |
|- ( ph -> -. U. dom O e. ( `' O ` X ) ) |
450 |
|
isorel |
|- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( U. dom O e. dom O /\ ( `' O ` X ) e. dom O ) ) -> ( U. dom O _E ( `' O ` X ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) ) ) |
451 |
47 45 53 450
|
syl12anc |
|- ( ph -> ( U. dom O _E ( `' O ` X ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) ) ) |
452 |
|
fvex |
|- ( `' O ` X ) e. _V |
453 |
452
|
epeli |
|- ( U. dom O _E ( `' O ` X ) <-> U. dom O e. ( `' O ` X ) ) |
454 |
|
fvex |
|- ( O ` ( `' O ` X ) ) e. _V |
455 |
454
|
epeli |
|- ( ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) ) |
456 |
451 453 455
|
3bitr3g |
|- ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) ) ) |
457 |
109
|
eleq2d |
|- ( ph -> ( ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. X ) ) |
458 |
456 457
|
bitrd |
|- ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. X ) ) |
459 |
449 458
|
mtbid |
|- ( ph -> -. ( O ` U. dom O ) e. X ) |
460 |
|
onelon |
|- ( ( B e. On /\ X e. B ) -> X e. On ) |
461 |
3 161 460
|
syl2anc |
|- ( ph -> X e. On ) |
462 |
|
ontri1 |
|- ( ( X e. On /\ ( O ` U. dom O ) e. On ) -> ( X C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. X ) ) |
463 |
461 436 462
|
syl2anc |
|- ( ph -> ( X C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. X ) ) |
464 |
459 463
|
mpbird |
|- ( ph -> X C_ ( O ` U. dom O ) ) |
465 |
464
|
adantr |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> X C_ ( O ` U. dom O ) ) |
466 |
|
simprr |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( O ` U. dom O ) e. x ) |
467 |
224
|
adantrr |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. On ) |
468 |
|
ontr2 |
|- ( ( X e. On /\ x e. On ) -> ( ( X C_ ( O ` U. dom O ) /\ ( O ` U. dom O ) e. x ) -> X e. x ) ) |
469 |
461 467 468
|
syl2an2r |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( ( X C_ ( O ` U. dom O ) /\ ( O ` U. dom O ) e. x ) -> X e. x ) ) |
470 |
465 466 469
|
mp2and |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> X e. x ) |
471 |
|
eleq2 |
|- ( w = x -> ( X e. w <-> X e. x ) ) |
472 |
|
fveq2 |
|- ( w = x -> ( F ` w ) = ( F ` x ) ) |
473 |
|
fveq2 |
|- ( w = x -> ( G ` w ) = ( G ` x ) ) |
474 |
472 473
|
eqeq12d |
|- ( w = x -> ( ( F ` w ) = ( G ` w ) <-> ( F ` x ) = ( G ` x ) ) ) |
475 |
471 474
|
imbi12d |
|- ( w = x -> ( ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> ( X e. x -> ( F ` x ) = ( G ` x ) ) ) ) |
476 |
475
|
rspcv |
|- ( x e. B -> ( A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) -> ( X e. x -> ( F ` x ) = ( G ` x ) ) ) ) |
477 |
441 442 470 476
|
syl3c |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( F ` x ) = ( G ` x ) ) |
478 |
466
|
adantr |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( O ` U. dom O ) e. x ) |
479 |
47
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) ) |
480 |
45
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> U. dom O e. dom O ) |
481 |
52
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> `' O : ( G supp (/) ) --> dom O ) |
482 |
|
ffvelrn |
|- ( ( `' O : ( G supp (/) ) --> dom O /\ x e. ( G supp (/) ) ) -> ( `' O ` x ) e. dom O ) |
483 |
481 482
|
sylancom |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( `' O ` x ) e. dom O ) |
484 |
|
isorel |
|- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( U. dom O e. dom O /\ ( `' O ` x ) e. dom O ) ) -> ( U. dom O _E ( `' O ` x ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` x ) ) ) ) |
485 |
479 480 483 484
|
syl12anc |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( U. dom O _E ( `' O ` x ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` x ) ) ) ) |
486 |
269
|
epeli |
|- ( U. dom O _E ( `' O ` x ) <-> U. dom O e. ( `' O ` x ) ) |
487 |
271
|
epeli |
|- ( ( O ` U. dom O ) _E ( O ` ( `' O ` x ) ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) ) |
488 |
485 486 487
|
3bitr3g |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( U. dom O e. ( `' O ` x ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) ) ) |
489 |
49
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) ) |
490 |
489 261
|
sylancom |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( O ` ( `' O ` x ) ) = x ) |
491 |
490
|
eleq2d |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) <-> ( O ` U. dom O ) e. x ) ) |
492 |
488 491
|
bitrd |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( U. dom O e. ( `' O ` x ) <-> ( O ` U. dom O ) e. x ) ) |
493 |
478 492
|
mpbird |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> U. dom O e. ( `' O ` x ) ) |
494 |
|
elssuni |
|- ( ( `' O ` x ) e. dom O -> ( `' O ` x ) C_ U. dom O ) |
495 |
483 494
|
syl |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( `' O ` x ) C_ U. dom O ) |
496 |
37 483 275
|
sylancr |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( `' O ` x ) e. On ) |
497 |
496 277
|
syl |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> Ord ( `' O ` x ) ) |
498 |
|
ordtri1 |
|- ( ( Ord ( `' O ` x ) /\ Ord U. dom O ) -> ( ( `' O ` x ) C_ U. dom O <-> -. U. dom O e. ( `' O ` x ) ) ) |
499 |
497 446 498
|
sylancl |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> ( ( `' O ` x ) C_ U. dom O <-> -. U. dom O e. ( `' O ` x ) ) ) |
500 |
495 499
|
mpbid |
|- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( G supp (/) ) ) -> -. U. dom O e. ( `' O ` x ) ) |
501 |
493 500
|
pm2.65da |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> -. x e. ( G supp (/) ) ) |
502 |
441 501
|
eldifd |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. ( B \ ( G supp (/) ) ) ) |
503 |
|
ssidd |
|- ( ph -> ( G supp (/) ) C_ ( G supp (/) ) ) |
504 |
159 503 3 176
|
suppssr |
|- ( ( ph /\ x e. ( B \ ( G supp (/) ) ) ) -> ( G ` x ) = (/) ) |
505 |
502 504
|
syldan |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( G ` x ) = (/) ) |
506 |
477 505
|
eqtrd |
|- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( F ` x ) = (/) ) |
507 |
506
|
expr |
|- ( ( ph /\ x e. B ) -> ( ( O ` U. dom O ) e. x -> ( F ` x ) = (/) ) ) |
508 |
440 507
|
sylbird |
|- ( ( ph /\ x e. B ) -> ( -. x C_ ( O ` U. dom O ) -> ( F ` x ) = (/) ) ) |
509 |
508
|
imp |
|- ( ( ( ph /\ x e. B ) /\ -. x C_ ( O ` U. dom O ) ) -> ( F ` x ) = (/) ) |
510 |
429 430 431 509
|
ifbothda |
|- ( ( ph /\ x e. B ) -> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) |
511 |
510
|
mpteq2dva |
|- ( ph -> ( x e. B |-> ( F ` x ) ) = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) |
512 |
428 511
|
eqtrd |
|- ( ph -> F = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) |
513 |
512
|
fveq2d |
|- ( ph -> ( ( A CNF B ) ` F ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) ) |
514 |
1 2 3 9 6 10
|
cantnfval |
|- ( ph -> ( ( A CNF B ) ` G ) = ( H ` dom O ) ) |
515 |
44
|
fveq2d |
|- ( ph -> ( H ` dom O ) = ( H ` suc U. dom O ) ) |
516 |
514 515
|
eqtrd |
|- ( ph -> ( ( A CNF B ) ` G ) = ( H ` suc U. dom O ) ) |
517 |
427 513 516
|
3eltr4d |
|- ( ph -> ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` G ) ) |