Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . 3
โข ๐ = dom (๐ด CNF ๐ต) |
2 | | cantnfs.a |
. . 3
โข (๐ โ ๐ด โ On) |
3 | | cantnfs.b |
. . 3
โข (๐ โ ๐ต โ On) |
4 | | eqid 2733 |
. . 3
โข OrdIso( E
, (๐น supp โ
)) =
OrdIso( E , (๐น supp
โ
)) |
5 | | cantnflt2.f |
. . 3
โข (๐ โ ๐น โ ๐) |
6 | | eqid 2733 |
. . 3
โข
seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E , (๐น supp โ
))โ๐)) ยทo (๐นโ(OrdIso( E , (๐น supp โ
))โ๐))) +o ๐ง)), โ
) =
seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , (๐น supp โ
))โ๐)) ยทo (๐นโ(OrdIso( E , (๐น supp โ
))โ๐))) +o ๐ง)), โ
) |
7 | 1, 2, 3, 4, 5, 6 | cantnfval 9612 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = (seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (OrdIso( E , (๐น supp โ
))โ๐)) ยทo (๐นโ(OrdIso( E , (๐น supp โ
))โ๐))) +o ๐ง)), โ
)โdom OrdIso( E
, (๐น supp
โ
)))) |
8 | | cantnflt2.a |
. . 3
โข (๐ โ โ
โ ๐ด) |
9 | | ovexd 7396 |
. . . 4
โข (๐ โ (๐น supp โ
) โ V) |
10 | 4 | oion 9480 |
. . . 4
โข ((๐น supp โ
) โ V โ
dom OrdIso( E , (๐น supp
โ
)) โ On) |
11 | | sucidg 6402 |
. . . 4
โข (dom
OrdIso( E , (๐น supp
โ
)) โ On โ dom OrdIso( E , (๐น supp โ
)) โ suc dom OrdIso( E ,
(๐น supp
โ
))) |
12 | 9, 10, 11 | 3syl 18 |
. . 3
โข (๐ โ dom OrdIso( E , (๐น supp โ
)) โ suc dom
OrdIso( E , (๐น supp
โ
))) |
13 | | cantnflt2.c |
. . 3
โข (๐ โ ๐ถ โ On) |
14 | 1, 2, 3, 4, 5 | cantnfcl 9611 |
. . . . . . 7
โข (๐ โ ( E We (๐น supp โ
) โง dom OrdIso( E , (๐น supp โ
)) โ
ฯ)) |
15 | 14 | simpld 496 |
. . . . . 6
โข (๐ โ E We (๐น supp โ
)) |
16 | 4 | oiiso 9481 |
. . . . . 6
โข (((๐น supp โ
) โ V โง E
We (๐น supp โ
)) โ
OrdIso( E , (๐น supp
โ
)) Isom E , E (dom OrdIso( E , (๐น supp โ
)), (๐น supp โ
))) |
17 | 9, 15, 16 | syl2anc 585 |
. . . . 5
โข (๐ โ OrdIso( E , (๐น supp โ
)) Isom E , E (dom
OrdIso( E , (๐น supp
โ
)), (๐น supp
โ
))) |
18 | | isof1o 7272 |
. . . . 5
โข (OrdIso(
E , (๐น supp โ
)) Isom
E , E (dom OrdIso( E , (๐น
supp โ
)), (๐น supp
โ
)) โ OrdIso( E , (๐น supp โ
)):dom OrdIso( E , (๐น supp โ
))โ1-1-ontoโ(๐น supp โ
)) |
19 | | f1ofo 6795 |
. . . . 5
โข (OrdIso(
E , (๐น supp โ
)):dom
OrdIso( E , (๐น supp
โ
))โ1-1-ontoโ(๐น supp โ
) โ OrdIso( E , (๐น supp โ
)):dom OrdIso( E ,
(๐น supp
โ
))โontoโ(๐น supp โ
)) |
20 | | foima 6765 |
. . . . 5
โข (OrdIso(
E , (๐น supp โ
)):dom
OrdIso( E , (๐น supp
โ
))โontoโ(๐น supp โ
) โ (OrdIso( E
, (๐น supp โ
)) โ
dom OrdIso( E , (๐น supp
โ
))) = (๐น supp
โ
)) |
21 | 17, 18, 19, 20 | 4syl 19 |
. . . 4
โข (๐ โ (OrdIso( E , (๐น supp โ
)) โ dom
OrdIso( E , (๐น supp
โ
))) = (๐น supp
โ
)) |
22 | | cantnflt2.s |
. . . 4
โข (๐ โ (๐น supp โ
) โ ๐ถ) |
23 | 21, 22 | eqsstrd 3986 |
. . 3
โข (๐ โ (OrdIso( E , (๐น supp โ
)) โ dom
OrdIso( E , (๐น supp
โ
))) โ ๐ถ) |
24 | 1, 2, 3, 4, 5, 6, 8, 12, 13, 23 | cantnflt 9616 |
. 2
โข (๐ โ
(seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (OrdIso( E , (๐น supp โ
))โ๐)) ยทo (๐นโ(OrdIso( E , (๐น supp โ
))โ๐))) +o ๐ง)), โ
)โdom OrdIso( E , (๐น supp โ
))) โ (๐ด โo ๐ถ)) |
25 | 7, 24 | eqeltrd 2834 |
1
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) โ (๐ด โo ๐ถ)) |