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 |
|
cantnfp1.g |
|- ( ph -> G e. S ) |
5 |
|
cantnfp1.x |
|- ( ph -> X e. B ) |
6 |
|
cantnfp1.y |
|- ( ph -> Y e. A ) |
7 |
|
cantnfp1.s |
|- ( ph -> ( G supp (/) ) C_ X ) |
8 |
|
cantnfp1.f |
|- F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) ) |
9 |
6
|
adantr |
|- ( ( ph /\ t e. B ) -> Y e. A ) |
10 |
1 2 3
|
cantnfs |
|- ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) ) |
11 |
4 10
|
mpbid |
|- ( ph -> ( G : B --> A /\ G finSupp (/) ) ) |
12 |
11
|
simpld |
|- ( ph -> G : B --> A ) |
13 |
12
|
ffvelrnda |
|- ( ( ph /\ t e. B ) -> ( G ` t ) e. A ) |
14 |
9 13
|
ifcld |
|- ( ( ph /\ t e. B ) -> if ( t = X , Y , ( G ` t ) ) e. A ) |
15 |
14 8
|
fmptd |
|- ( ph -> F : B --> A ) |
16 |
11
|
simprd |
|- ( ph -> G finSupp (/) ) |
17 |
16
|
fsuppimpd |
|- ( ph -> ( G supp (/) ) e. Fin ) |
18 |
|
snfi |
|- { X } e. Fin |
19 |
|
unfi |
|- ( ( ( G supp (/) ) e. Fin /\ { X } e. Fin ) -> ( ( G supp (/) ) u. { X } ) e. Fin ) |
20 |
17 18 19
|
sylancl |
|- ( ph -> ( ( G supp (/) ) u. { X } ) e. Fin ) |
21 |
|
eqeq1 |
|- ( t = k -> ( t = X <-> k = X ) ) |
22 |
|
fveq2 |
|- ( t = k -> ( G ` t ) = ( G ` k ) ) |
23 |
21 22
|
ifbieq2d |
|- ( t = k -> if ( t = X , Y , ( G ` t ) ) = if ( k = X , Y , ( G ` k ) ) ) |
24 |
|
eldifi |
|- ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> k e. B ) |
25 |
24
|
adantl |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> k e. B ) |
26 |
6
|
adantr |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> Y e. A ) |
27 |
|
fvex |
|- ( G ` k ) e. _V |
28 |
|
ifexg |
|- ( ( Y e. A /\ ( G ` k ) e. _V ) -> if ( k = X , Y , ( G ` k ) ) e. _V ) |
29 |
26 27 28
|
sylancl |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> if ( k = X , Y , ( G ` k ) ) e. _V ) |
30 |
8 23 25 29
|
fvmptd3 |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( F ` k ) = if ( k = X , Y , ( G ` k ) ) ) |
31 |
|
eldifn |
|- ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> -. k e. ( ( G supp (/) ) u. { X } ) ) |
32 |
31
|
adantl |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> -. k e. ( ( G supp (/) ) u. { X } ) ) |
33 |
|
velsn |
|- ( k e. { X } <-> k = X ) |
34 |
|
elun2 |
|- ( k e. { X } -> k e. ( ( G supp (/) ) u. { X } ) ) |
35 |
33 34
|
sylbir |
|- ( k = X -> k e. ( ( G supp (/) ) u. { X } ) ) |
36 |
32 35
|
nsyl |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> -. k = X ) |
37 |
36
|
iffalsed |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> if ( k = X , Y , ( G ` k ) ) = ( G ` k ) ) |
38 |
|
ssun1 |
|- ( G supp (/) ) C_ ( ( G supp (/) ) u. { X } ) |
39 |
|
sscon |
|- ( ( G supp (/) ) C_ ( ( G supp (/) ) u. { X } ) -> ( B \ ( ( G supp (/) ) u. { X } ) ) C_ ( B \ ( G supp (/) ) ) ) |
40 |
38 39
|
ax-mp |
|- ( B \ ( ( G supp (/) ) u. { X } ) ) C_ ( B \ ( G supp (/) ) ) |
41 |
40
|
sseli |
|- ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> k e. ( B \ ( G supp (/) ) ) ) |
42 |
|
ssidd |
|- ( ph -> ( G supp (/) ) C_ ( G supp (/) ) ) |
43 |
|
0ex |
|- (/) e. _V |
44 |
43
|
a1i |
|- ( ph -> (/) e. _V ) |
45 |
12 42 3 44
|
suppssr |
|- ( ( ph /\ k e. ( B \ ( G supp (/) ) ) ) -> ( G ` k ) = (/) ) |
46 |
41 45
|
sylan2 |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( G ` k ) = (/) ) |
47 |
30 37 46
|
3eqtrd |
|- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( F ` k ) = (/) ) |
48 |
15 47
|
suppss |
|- ( ph -> ( F supp (/) ) C_ ( ( G supp (/) ) u. { X } ) ) |
49 |
20 48
|
ssfid |
|- ( ph -> ( F supp (/) ) e. Fin ) |
50 |
8
|
funmpt2 |
|- Fun F |
51 |
|
mptexg |
|- ( B e. On -> ( t e. B |-> if ( t = X , Y , ( G ` t ) ) ) e. _V ) |
52 |
8 51
|
eqeltrid |
|- ( B e. On -> F e. _V ) |
53 |
3 52
|
syl |
|- ( ph -> F e. _V ) |
54 |
|
funisfsupp |
|- ( ( Fun F /\ F e. _V /\ (/) e. _V ) -> ( F finSupp (/) <-> ( F supp (/) ) e. Fin ) ) |
55 |
50 53 44 54
|
mp3an2i |
|- ( ph -> ( F finSupp (/) <-> ( F supp (/) ) e. Fin ) ) |
56 |
49 55
|
mpbird |
|- ( ph -> F finSupp (/) ) |
57 |
1 2 3
|
cantnfs |
|- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) ) |
58 |
15 56 57
|
mpbir2and |
|- ( ph -> F e. S ) |