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 |
1 2 3 4
|
oemapso |
|- ( ph -> T Or S ) |
6 |
|
oecl |
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On ) |
7 |
2 3 6
|
syl2anc |
|- ( ph -> ( A ^o B ) e. On ) |
8 |
|
eloni |
|- ( ( A ^o B ) e. On -> Ord ( A ^o B ) ) |
9 |
7 8
|
syl |
|- ( ph -> Ord ( A ^o B ) ) |
10 |
|
ordwe |
|- ( Ord ( A ^o B ) -> _E We ( A ^o B ) ) |
11 |
|
weso |
|- ( _E We ( A ^o B ) -> _E Or ( A ^o B ) ) |
12 |
|
sopo |
|- ( _E Or ( A ^o B ) -> _E Po ( A ^o B ) ) |
13 |
9 10 11 12
|
4syl |
|- ( ph -> _E Po ( A ^o B ) ) |
14 |
1 2 3
|
cantnff |
|- ( ph -> ( A CNF B ) : S --> ( A ^o B ) ) |
15 |
14
|
frnd |
|- ( ph -> ran ( A CNF B ) C_ ( A ^o B ) ) |
16 |
|
onss |
|- ( ( A ^o B ) e. On -> ( A ^o B ) C_ On ) |
17 |
7 16
|
syl |
|- ( ph -> ( A ^o B ) C_ On ) |
18 |
17
|
sseld |
|- ( ph -> ( t e. ( A ^o B ) -> t e. On ) ) |
19 |
|
eleq1w |
|- ( t = y -> ( t e. ( A ^o B ) <-> y e. ( A ^o B ) ) ) |
20 |
|
eleq1w |
|- ( t = y -> ( t e. ran ( A CNF B ) <-> y e. ran ( A CNF B ) ) ) |
21 |
19 20
|
imbi12d |
|- ( t = y -> ( ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) <-> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) ) |
22 |
21
|
imbi2d |
|- ( t = y -> ( ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) <-> ( ph -> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) ) ) |
23 |
|
r19.21v |
|- ( A. y e. t ( ph -> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) <-> ( ph -> A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) ) |
24 |
|
ordelss |
|- ( ( Ord ( A ^o B ) /\ t e. ( A ^o B ) ) -> t C_ ( A ^o B ) ) |
25 |
9 24
|
sylan |
|- ( ( ph /\ t e. ( A ^o B ) ) -> t C_ ( A ^o B ) ) |
26 |
25
|
sselda |
|- ( ( ( ph /\ t e. ( A ^o B ) ) /\ y e. t ) -> y e. ( A ^o B ) ) |
27 |
|
pm5.5 |
|- ( y e. ( A ^o B ) -> ( ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> y e. ran ( A CNF B ) ) ) |
28 |
26 27
|
syl |
|- ( ( ( ph /\ t e. ( A ^o B ) ) /\ y e. t ) -> ( ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> y e. ran ( A CNF B ) ) ) |
29 |
28
|
ralbidva |
|- ( ( ph /\ t e. ( A ^o B ) ) -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> A. y e. t y e. ran ( A CNF B ) ) ) |
30 |
|
dfss3 |
|- ( t C_ ran ( A CNF B ) <-> A. y e. t y e. ran ( A CNF B ) ) |
31 |
29 30
|
bitr4di |
|- ( ( ph /\ t e. ( A ^o B ) ) -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> t C_ ran ( A CNF B ) ) ) |
32 |
|
eleq1 |
|- ( t = (/) -> ( t e. ran ( A CNF B ) <-> (/) e. ran ( A CNF B ) ) ) |
33 |
2
|
adantr |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> A e. On ) |
34 |
33
|
adantr |
|- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> A e. On ) |
35 |
3
|
adantr |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> B e. On ) |
36 |
35
|
adantr |
|- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> B e. On ) |
37 |
|
simplrl |
|- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t e. ( A ^o B ) ) |
38 |
|
simplrr |
|- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t C_ ran ( A CNF B ) ) |
39 |
7
|
adantr |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A ^o B ) e. On ) |
40 |
|
simprl |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. ( A ^o B ) ) |
41 |
|
onelon |
|- ( ( ( A ^o B ) e. On /\ t e. ( A ^o B ) ) -> t e. On ) |
42 |
39 40 41
|
syl2anc |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. On ) |
43 |
|
on0eln0 |
|- ( t e. On -> ( (/) e. t <-> t =/= (/) ) ) |
44 |
42 43
|
syl |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( (/) e. t <-> t =/= (/) ) ) |
45 |
44
|
biimpar |
|- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> (/) e. t ) |
46 |
|
eqid |
|- U. |^| { c e. On | t e. ( A ^o c ) } = U. |^| { c e. On | t e. ( A ^o c ) } |
47 |
|
eqid |
|- ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) = ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) |
48 |
|
eqid |
|- ( 1st ` ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) ) = ( 1st ` ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) ) |
49 |
|
eqid |
|- ( 2nd ` ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) ) = ( 2nd ` ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) ) |
50 |
1 34 36 4 37 38 45 46 47 48 49
|
cantnflem4 |
|- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t e. ran ( A CNF B ) ) |
51 |
|
fczsupp0 |
|- ( ( B X. { (/) } ) supp (/) ) = (/) |
52 |
51
|
eqcomi |
|- (/) = ( ( B X. { (/) } ) supp (/) ) |
53 |
|
oieq2 |
|- ( (/) = ( ( B X. { (/) } ) supp (/) ) -> OrdIso ( _E , (/) ) = OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) ) |
54 |
52 53
|
ax-mp |
|- OrdIso ( _E , (/) ) = OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) |
55 |
|
ne0i |
|- ( t e. ( A ^o B ) -> ( A ^o B ) =/= (/) ) |
56 |
55
|
ad2antrl |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A ^o B ) =/= (/) ) |
57 |
|
oveq1 |
|- ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) ) |
58 |
57
|
neeq1d |
|- ( A = (/) -> ( ( A ^o B ) =/= (/) <-> ( (/) ^o B ) =/= (/) ) ) |
59 |
56 58
|
syl5ibcom |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A = (/) -> ( (/) ^o B ) =/= (/) ) ) |
60 |
59
|
necon2d |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( (/) ^o B ) = (/) -> A =/= (/) ) ) |
61 |
|
on0eln0 |
|- ( B e. On -> ( (/) e. B <-> B =/= (/) ) ) |
62 |
|
oe0m1 |
|- ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) ) |
63 |
61 62
|
bitr3d |
|- ( B e. On -> ( B =/= (/) <-> ( (/) ^o B ) = (/) ) ) |
64 |
35 63
|
syl |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B =/= (/) <-> ( (/) ^o B ) = (/) ) ) |
65 |
|
on0eln0 |
|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) ) |
66 |
33 65
|
syl |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( (/) e. A <-> A =/= (/) ) ) |
67 |
60 64 66
|
3imtr4d |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B =/= (/) -> (/) e. A ) ) |
68 |
|
ne0i |
|- ( y e. B -> B =/= (/) ) |
69 |
67 68
|
impel |
|- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ y e. B ) -> (/) e. A ) |
70 |
|
fconstmpt |
|- ( B X. { (/) } ) = ( y e. B |-> (/) ) |
71 |
69 70
|
fmptd |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B X. { (/) } ) : B --> A ) |
72 |
|
0ex |
|- (/) e. _V |
73 |
72
|
a1i |
|- ( ph -> (/) e. _V ) |
74 |
3 73
|
fczfsuppd |
|- ( ph -> ( B X. { (/) } ) finSupp (/) ) |
75 |
74
|
adantr |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B X. { (/) } ) finSupp (/) ) |
76 |
1 2 3
|
cantnfs |
|- ( ph -> ( ( B X. { (/) } ) e. S <-> ( ( B X. { (/) } ) : B --> A /\ ( B X. { (/) } ) finSupp (/) ) ) ) |
77 |
76
|
adantr |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( B X. { (/) } ) e. S <-> ( ( B X. { (/) } ) : B --> A /\ ( B X. { (/) } ) finSupp (/) ) ) ) |
78 |
71 75 77
|
mpbir2and |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B X. { (/) } ) e. S ) |
79 |
|
eqid |
|- seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) |
80 |
1 33 35 54 78 79
|
cantnfval |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) ) |
81 |
|
we0 |
|- _E We (/) |
82 |
|
eqid |
|- OrdIso ( _E , (/) ) = OrdIso ( _E , (/) ) |
83 |
82
|
oien |
|- ( ( (/) e. _V /\ _E We (/) ) -> dom OrdIso ( _E , (/) ) ~~ (/) ) |
84 |
72 81 83
|
mp2an |
|- dom OrdIso ( _E , (/) ) ~~ (/) |
85 |
|
en0 |
|- ( dom OrdIso ( _E , (/) ) ~~ (/) <-> dom OrdIso ( _E , (/) ) = (/) ) |
86 |
84 85
|
mpbi |
|- dom OrdIso ( _E , (/) ) = (/) |
87 |
86
|
fveq2i |
|- ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) |
88 |
79
|
seqom0g |
|- ( (/) e. _V -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) ) |
89 |
72 88
|
ax-mp |
|- ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) |
90 |
87 89
|
eqtri |
|- ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) = (/) |
91 |
80 90
|
eqtrdi |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = (/) ) |
92 |
14
|
adantr |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A CNF B ) : S --> ( A ^o B ) ) |
93 |
92
|
ffnd |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A CNF B ) Fn S ) |
94 |
|
fnfvelrn |
|- ( ( ( A CNF B ) Fn S /\ ( B X. { (/) } ) e. S ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) e. ran ( A CNF B ) ) |
95 |
93 78 94
|
syl2anc |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) e. ran ( A CNF B ) ) |
96 |
91 95
|
eqeltrrd |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> (/) e. ran ( A CNF B ) ) |
97 |
32 50 96
|
pm2.61ne |
|- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. ran ( A CNF B ) ) |
98 |
97
|
expr |
|- ( ( ph /\ t e. ( A ^o B ) ) -> ( t C_ ran ( A CNF B ) -> t e. ran ( A CNF B ) ) ) |
99 |
31 98
|
sylbid |
|- ( ( ph /\ t e. ( A ^o B ) ) -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) -> t e. ran ( A CNF B ) ) ) |
100 |
99
|
ex |
|- ( ph -> ( t e. ( A ^o B ) -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) -> t e. ran ( A CNF B ) ) ) ) |
101 |
100
|
com23 |
|- ( ph -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) ) |
102 |
101
|
a2i |
|- ( ( ph -> A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) ) |
103 |
102
|
a1i |
|- ( t e. On -> ( ( ph -> A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) ) ) |
104 |
23 103
|
syl5bi |
|- ( t e. On -> ( A. y e. t ( ph -> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) ) ) |
105 |
22 104
|
tfis2 |
|- ( t e. On -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) ) |
106 |
105
|
com3l |
|- ( ph -> ( t e. ( A ^o B ) -> ( t e. On -> t e. ran ( A CNF B ) ) ) ) |
107 |
18 106
|
mpdd |
|- ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) |
108 |
107
|
ssrdv |
|- ( ph -> ( A ^o B ) C_ ran ( A CNF B ) ) |
109 |
15 108
|
eqssd |
|- ( ph -> ran ( A CNF B ) = ( A ^o B ) ) |
110 |
|
dffo2 |
|- ( ( A CNF B ) : S -onto-> ( A ^o B ) <-> ( ( A CNF B ) : S --> ( A ^o B ) /\ ran ( A CNF B ) = ( A ^o B ) ) ) |
111 |
14 109 110
|
sylanbrc |
|- ( ph -> ( A CNF B ) : S -onto-> ( A ^o B ) ) |
112 |
2
|
adantr |
|- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> A e. On ) |
113 |
3
|
adantr |
|- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> B e. On ) |
114 |
|
fveq2 |
|- ( z = t -> ( x ` z ) = ( x ` t ) ) |
115 |
|
fveq2 |
|- ( z = t -> ( y ` z ) = ( y ` t ) ) |
116 |
114 115
|
eleq12d |
|- ( z = t -> ( ( x ` z ) e. ( y ` z ) <-> ( x ` t ) e. ( y ` t ) ) ) |
117 |
|
eleq1w |
|- ( z = t -> ( z e. w <-> t e. w ) ) |
118 |
117
|
imbi1d |
|- ( z = t -> ( ( z e. w -> ( x ` w ) = ( y ` w ) ) <-> ( t e. w -> ( x ` w ) = ( y ` w ) ) ) ) |
119 |
118
|
ralbidv |
|- ( z = t -> ( A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) ) |
120 |
116 119
|
anbi12d |
|- ( z = t -> ( ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` t ) e. ( y ` t ) /\ A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) ) ) |
121 |
120
|
cbvrexvw |
|- ( E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) <-> E. t e. B ( ( x ` t ) e. ( y ` t ) /\ A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) ) |
122 |
|
fveq1 |
|- ( x = u -> ( x ` t ) = ( u ` t ) ) |
123 |
|
fveq1 |
|- ( y = v -> ( y ` t ) = ( v ` t ) ) |
124 |
|
eleq12 |
|- ( ( ( x ` t ) = ( u ` t ) /\ ( y ` t ) = ( v ` t ) ) -> ( ( x ` t ) e. ( y ` t ) <-> ( u ` t ) e. ( v ` t ) ) ) |
125 |
122 123 124
|
syl2an |
|- ( ( x = u /\ y = v ) -> ( ( x ` t ) e. ( y ` t ) <-> ( u ` t ) e. ( v ` t ) ) ) |
126 |
|
fveq1 |
|- ( x = u -> ( x ` w ) = ( u ` w ) ) |
127 |
|
fveq1 |
|- ( y = v -> ( y ` w ) = ( v ` w ) ) |
128 |
126 127
|
eqeqan12d |
|- ( ( x = u /\ y = v ) -> ( ( x ` w ) = ( y ` w ) <-> ( u ` w ) = ( v ` w ) ) ) |
129 |
128
|
imbi2d |
|- ( ( x = u /\ y = v ) -> ( ( t e. w -> ( x ` w ) = ( y ` w ) ) <-> ( t e. w -> ( u ` w ) = ( v ` w ) ) ) ) |
130 |
129
|
ralbidv |
|- ( ( x = u /\ y = v ) -> ( A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) ) |
131 |
125 130
|
anbi12d |
|- ( ( x = u /\ y = v ) -> ( ( ( x ` t ) e. ( y ` t ) /\ A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) ) ) |
132 |
131
|
rexbidv |
|- ( ( x = u /\ y = v ) -> ( E. t e. B ( ( x ` t ) e. ( y ` t ) /\ A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) <-> E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) ) ) |
133 |
121 132
|
syl5bb |
|- ( ( x = u /\ y = v ) -> ( E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) <-> E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) ) ) |
134 |
133
|
cbvopabv |
|- { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } = { <. u , v >. | E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) } |
135 |
4 134
|
eqtri |
|- T = { <. u , v >. | E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) } |
136 |
|
simprll |
|- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> f e. S ) |
137 |
|
simprlr |
|- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> g e. S ) |
138 |
|
simprr |
|- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> f T g ) |
139 |
|
eqid |
|- U. { c e. B | ( f ` c ) e. ( g ` c ) } = U. { c e. B | ( f ` c ) e. ( g ` c ) } |
140 |
|
eqid |
|- OrdIso ( _E , ( g supp (/) ) ) = OrdIso ( _E , ( g supp (/) ) ) |
141 |
|
eqid |
|- seqom ( ( k e. _V , t e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( g supp (/) ) ) ` k ) ) .o ( g ` ( OrdIso ( _E , ( g supp (/) ) ) ` k ) ) ) +o t ) ) , (/) ) = seqom ( ( k e. _V , t e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( g supp (/) ) ) ` k ) ) .o ( g ` ( OrdIso ( _E , ( g supp (/) ) ) ` k ) ) ) +o t ) ) , (/) ) |
142 |
1 112 113 135 136 137 138 139 140 141
|
cantnflem1 |
|- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> ( ( A CNF B ) ` f ) e. ( ( A CNF B ) ` g ) ) |
143 |
|
fvex |
|- ( ( A CNF B ) ` g ) e. _V |
144 |
143
|
epeli |
|- ( ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) <-> ( ( A CNF B ) ` f ) e. ( ( A CNF B ) ` g ) ) |
145 |
142 144
|
sylibr |
|- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) |
146 |
145
|
expr |
|- ( ( ph /\ ( f e. S /\ g e. S ) ) -> ( f T g -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) ) |
147 |
146
|
ralrimivva |
|- ( ph -> A. f e. S A. g e. S ( f T g -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) ) |
148 |
|
soisoi |
|- ( ( ( T Or S /\ _E Po ( A ^o B ) ) /\ ( ( A CNF B ) : S -onto-> ( A ^o B ) /\ A. f e. S A. g e. S ( f T g -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) ) ) -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) ) |
149 |
5 13 111 147 148
|
syl22anc |
|- ( ph -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) ) |