Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
โข dom
(ฯ CNF ๐ด) = dom
(ฯ CNF ๐ด) |
2 | | eqid 2733 |
. 2
โข (โก(ฯ CNF ๐ด)โ๐) = (โก(ฯ CNF ๐ด)โ๐) |
3 | | eqid 2733 |
. 2
โข OrdIso( E
, ((โก(ฯ CNF ๐ด)โ๐) supp โ
)) = OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)) |
4 | | eqid 2733 |
. 2
โข
seqฯ((๐ โ V, ๐ง โ V โฆ (((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ง)), โ
) = seqฯ((๐ โ V, ๐ง โ V โฆ (((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ง)), โ
) |
5 | | eqid 2733 |
. 2
โข
seqฯ((๐ โ V, ๐ โ V โฆ ((๐ฅ โ ((ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (((ฯ โo
(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ฅ)))), โ
) = seqฯ((๐ โ V, ๐ โ V โฆ ((๐ฅ โ ((ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (((ฯ โo
(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ฅ)))), โ
) |
6 | | eqid 2733 |
. 2
โข ((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) = ((ฯ โo (OrdIso( E
, ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) |
7 | | eqid 2733 |
. 2
โข ((๐ฅ โ ((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (((ฯ โo
(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ฅ))) = ((๐ฅ โ ((ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (((ฯ โo
(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ฅ))) |
8 | | eqid 2733 |
. 2
โข (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))) = (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))) |
9 | | eqid 2733 |
. 2
โข (๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ ((((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ฃ) +o ๐ข)) = (๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ ((((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ฃ) +o ๐ข)) |
10 | | eqid 2733 |
. 2
โข (๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ (((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ข) +o ๐ฃ)) = (๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ (((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ข) +o ๐ฃ)) |
11 | | eqid 2733 |
. 2
โข (((๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ ((((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ฃ) +o ๐ข)) โ โก(๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ (((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ข) +o ๐ฃ))) โ
(seqฯ((๐
โ V, ๐ โ V
โฆ ((๐ฅ โ
((ฯ โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (((ฯ โo
(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ฅ)))), โ
)โdom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) = (((๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ ((((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ฃ) +o ๐ข)) โ โก(๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ (((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ข) +o ๐ฃ))) โ
(seqฯ((๐
โ V, ๐ โ V
โฆ ((๐ฅ โ
((ฯ โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (((ฯ โo
(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ฅ)))), โ
)โdom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) |
12 | | eqid 2733 |
. 2
โข (๐ โ (ฯ
โo ๐ด)
โฆ (((๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ ((((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ฃ) +o ๐ข)) โ โก(๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ (((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ข) +o ๐ฃ))) โ
(seqฯ((๐
โ V, ๐ โ V
โฆ ((๐ฅ โ
((ฯ โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (((ฯ โo
(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ฅ)))), โ
)โdom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))))) = (๐ โ (ฯ โo ๐ด) โฆ (((๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ ((((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ฃ) +o ๐ข)) โ โก(๐ข โ ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))), ๐ฃ โ (ฯ โo (OrdIso(
E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) โฆ (((ฯ
โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โโช dom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
)))) ยทo ๐ข) +o ๐ฃ))) โ
(seqฯ((๐
โ V, ๐ โ V
โฆ ((๐ฅ โ
((ฯ โo (OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) โฆ (dom ๐ +o ๐ฅ)) โช โก(๐ฅ โ dom ๐ โฆ (((ฯ โo
(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐)) ยทo ((โก(ฯ CNF ๐ด)โ๐)โ(OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))โ๐))) +o ๐ฅ)))), โ
)โdom OrdIso( E , ((โก(ฯ CNF ๐ด)โ๐) supp โ
))))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cnfcom3clem 9646 |
1
โข (๐ด โ On โ โ๐โ๐ โ ๐ด (ฯ โ ๐ โ โ๐ค โ (On โ 1o)(๐โ๐):๐โ1-1-ontoโ(ฯ โo ๐ค))) |