Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
โข ๐ = dom ( ๐ด CNF ๐ต ) |
2 |
|
cantnfs.a |
โข ( ๐ โ ๐ด โ On ) |
3 |
|
cantnfs.b |
โข ( ๐ โ ๐ต โ On ) |
4 |
|
fvex |
โข ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) โ V |
5 |
4
|
csbex |
โข โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) โ V |
6 |
5
|
a1i |
โข ( ( ๐ โง ๐ โ ๐ ) โ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) โ V ) |
7 |
|
eqid |
โข { ๐ โ ( ๐ด โm ๐ต ) โฃ ๐ finSupp โ
} = { ๐ โ ( ๐ด โm ๐ต ) โฃ ๐ finSupp โ
} |
8 |
7 2 3
|
cantnffval |
โข ( ๐ โ ( ๐ด CNF ๐ต ) = ( ๐ โ { ๐ โ ( ๐ด โm ๐ต ) โฃ ๐ finSupp โ
} โฆ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) ) ) |
9 |
7 2 3
|
cantnfdm |
โข ( ๐ โ dom ( ๐ด CNF ๐ต ) = { ๐ โ ( ๐ด โm ๐ต ) โฃ ๐ finSupp โ
} ) |
10 |
1 9
|
eqtrid |
โข ( ๐ โ ๐ = { ๐ โ ( ๐ด โm ๐ต ) โฃ ๐ finSupp โ
} ) |
11 |
10
|
mpteq1d |
โข ( ๐ โ ( ๐ โ ๐ โฆ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) ) = ( ๐ โ { ๐ โ ( ๐ด โm ๐ต ) โฃ ๐ finSupp โ
} โฆ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) ) ) |
12 |
8 11
|
eqtr4d |
โข ( ๐ โ ( ๐ด CNF ๐ต ) = ( ๐ โ ๐ โฆ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) ) ) |
13 |
2
|
adantr |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ๐ด โ On ) |
14 |
3
|
adantr |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ๐ต โ On ) |
15 |
|
eqid |
โข OrdIso ( E , ( ๐ฅ supp โ
) ) = OrdIso ( E , ( ๐ฅ supp โ
) ) |
16 |
|
simpr |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ๐ฅ โ ๐ ) |
17 |
|
eqid |
โข seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ยทo ( ๐ฅ โ ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ) +o ๐ง ) ) , โ
) = seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ยทo ( ๐ฅ โ ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ) +o ๐ง ) ) , โ
) |
18 |
1 13 14 15 16 17
|
cantnfval |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) = ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ยทo ( ๐ฅ โ ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) ) ) |
19 |
18
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) = ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ยทo ( ๐ฅ โ ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) ) ) |
20 |
|
ovex |
โข ( ๐ฅ supp โ
) โ V |
21 |
1 13 14 15 16
|
cantnfcl |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ( E We ( ๐ฅ supp โ
) โง dom OrdIso ( E , ( ๐ฅ supp โ
) ) โ ฯ ) ) |
22 |
21
|
simpld |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ E We ( ๐ฅ supp โ
) ) |
23 |
15
|
oien |
โข ( ( ( ๐ฅ supp โ
) โ V โง E We ( ๐ฅ supp โ
) ) โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) โ ( ๐ฅ supp โ
) ) |
24 |
20 22 23
|
sylancr |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) โ ( ๐ฅ supp โ
) ) |
25 |
24
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) โ ( ๐ฅ supp โ
) ) |
26 |
|
suppssdm |
โข ( ๐ฅ supp โ
) โ dom ๐ฅ |
27 |
1 2 3
|
cantnfs |
โข ( ๐ โ ( ๐ฅ โ ๐ โ ( ๐ฅ : ๐ต โถ ๐ด โง ๐ฅ finSupp โ
) ) ) |
28 |
27
|
simprbda |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ๐ฅ : ๐ต โถ ๐ด ) |
29 |
26 28
|
fssdm |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ( ๐ฅ supp โ
) โ ๐ต ) |
30 |
|
feq3 |
โข ( ๐ด = โ
โ ( ๐ฅ : ๐ต โถ ๐ด โ ๐ฅ : ๐ต โถ โ
) ) |
31 |
28 30
|
syl5ibcom |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ( ๐ด = โ
โ ๐ฅ : ๐ต โถ โ
) ) |
32 |
31
|
imp |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ๐ฅ : ๐ต โถ โ
) |
33 |
|
f00 |
โข ( ๐ฅ : ๐ต โถ โ
โ ( ๐ฅ = โ
โง ๐ต = โ
) ) |
34 |
32 33
|
sylib |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ๐ฅ = โ
โง ๐ต = โ
) ) |
35 |
34
|
simprd |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ๐ต = โ
) |
36 |
|
sseq0 |
โข ( ( ( ๐ฅ supp โ
) โ ๐ต โง ๐ต = โ
) โ ( ๐ฅ supp โ
) = โ
) |
37 |
29 35 36
|
syl2an2r |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ๐ฅ supp โ
) = โ
) |
38 |
25 37
|
breqtrd |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) โ โ
) |
39 |
|
en0 |
โข ( dom OrdIso ( E , ( ๐ฅ supp โ
) ) โ โ
โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) = โ
) |
40 |
38 39
|
sylib |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) = โ
) |
41 |
40
|
fveq2d |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ยทo ( ๐ฅ โ ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom OrdIso ( E , ( ๐ฅ supp โ
) ) ) = ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ยทo ( ๐ฅ โ ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ โ
) ) |
42 |
|
0ex |
โข โ
โ V |
43 |
17
|
seqom0g |
โข ( โ
โ V โ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ยทo ( ๐ฅ โ ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ โ
) = โ
) |
44 |
42 43
|
mp1i |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ยทo ( ๐ฅ โ ( OrdIso ( E , ( ๐ฅ supp โ
) ) โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ โ
) = โ
) |
45 |
19 41 44
|
3eqtrd |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) = โ
) |
46 |
|
el1o |
โข ( ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) โ 1o โ ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) = โ
) |
47 |
45 46
|
sylibr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) โ 1o ) |
48 |
35
|
oveq2d |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ๐ด โo ๐ต ) = ( ๐ด โo โ
) ) |
49 |
13
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ๐ด โ On ) |
50 |
|
oe0 |
โข ( ๐ด โ On โ ( ๐ด โo โ
) = 1o ) |
51 |
49 50
|
syl |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ๐ด โo โ
) = 1o ) |
52 |
48 51
|
eqtrd |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ๐ด โo ๐ต ) = 1o ) |
53 |
47 52
|
eleqtrrd |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด = โ
) โ ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) โ ( ๐ด โo ๐ต ) ) |
54 |
13
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด โ โ
) โ ๐ด โ On ) |
55 |
14
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด โ โ
) โ ๐ต โ On ) |
56 |
16
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด โ โ
) โ ๐ฅ โ ๐ ) |
57 |
|
on0eln0 |
โข ( ๐ด โ On โ ( โ
โ ๐ด โ ๐ด โ โ
) ) |
58 |
13 57
|
syl |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ( โ
โ ๐ด โ ๐ด โ โ
) ) |
59 |
58
|
biimpar |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด โ โ
) โ โ
โ ๐ด ) |
60 |
29
|
adantr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด โ โ
) โ ( ๐ฅ supp โ
) โ ๐ต ) |
61 |
1 54 55 56 59 55 60
|
cantnflt2 |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ด โ โ
) โ ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) โ ( ๐ด โo ๐ต ) ) |
62 |
53 61
|
pm2.61dane |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ( ( ๐ด CNF ๐ต ) โ ๐ฅ ) โ ( ๐ด โo ๐ต ) ) |
63 |
6 12 62
|
fmpt2d |
โข ( ๐ โ ( ๐ด CNF ๐ต ) : ๐ โถ ( ๐ด โo ๐ต ) ) |