Step | Hyp | Ref
| Expression |
1 | | infxpenc2.1 |
. 2
β’ (π β π΄ β On) |
2 | | infxpenc2.2 |
. 2
β’ (π β βπ β π΄ (Ο β π β βπ€ β (On β 1o)(πβπ):πβ1-1-ontoβ(Ο βo π€))) |
3 | | infxpenc2.3 |
. 2
β’ π = (β‘(π₯ β (On β 1o) β¦
(Ο βo π₯))βran (πβπ)) |
4 | | infxpenc2.4 |
. 2
β’ (π β πΉ:(Ο βo
2o)β1-1-ontoβΟ) |
5 | | infxpenc2.5 |
. 2
β’ (π β (πΉββ
) = β
) |
6 | | eqid 2733 |
. 2
β’ (π¦ β {π₯ β ((Ο βo
2o) βm π) β£ π₯ finSupp β
} β¦ (πΉ β (π¦ β β‘( I βΎ π)))) = (π¦ β {π₯ β ((Ο βo
2o) βm π) β£ π₯ finSupp β
} β¦ (πΉ β (π¦ β β‘( I βΎ π)))) |
7 | | eqid 2733 |
. 2
β’
(((Ο CNF π)
β (π¦ β {π₯ β ((Ο
βo 2o) βm π) β£ π₯ finSupp β
} β¦ (πΉ β (π¦ β β‘( I βΎ π))))) β β‘((Ο βo 2o)
CNF π)) = (((Ο CNF
π) β (π¦ β {π₯ β ((Ο βo
2o) βm π) β£ π₯ finSupp β
} β¦ (πΉ β (π¦ β β‘( I βΎ π))))) β β‘((Ο βo 2o)
CNF π)) |
8 | | eqid 2733 |
. 2
β’ (π¦ β {π₯ β (Ο βm (π Β·o
2o)) β£ π₯
finSupp β
} β¦ (( I βΎ Ο) β (π¦ β β‘((π§ β 2o, π€ β π β¦ ((2o
Β·o π€)
+o π§)) β
β‘(π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€)))))) = (π¦ β {π₯ β (Ο βm (π Β·o
2o)) β£ π₯
finSupp β
} β¦ (( I βΎ Ο) β (π¦ β β‘((π§ β 2o, π€ β π β¦ ((2o
Β·o π€)
+o π§)) β
β‘(π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€)))))) |
9 | | eqid 2733 |
. 2
β’ (π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€)) = (π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€)) |
10 | | eqid 2733 |
. 2
β’ (π§ β 2o, π€ β π β¦ ((2o
Β·o π€)
+o π§)) = (π§ β 2o, π€ β π β¦ ((2o
Β·o π€)
+o π§)) |
11 | | eqid 2733 |
. 2
β’
(((Ο CNF (2o Β·o π)) β (π¦ β {π₯ β (Ο βm (π Β·o
2o)) β£ π₯
finSupp β
} β¦ (( I βΎ Ο) β (π¦ β β‘((π§ β 2o, π€ β π β¦ ((2o
Β·o π€)
+o π§)) β
β‘(π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€))))))) β β‘(Ο CNF (π Β·o 2o))) =
(((Ο CNF (2o Β·o π)) β (π¦ β {π₯ β (Ο βm (π Β·o
2o)) β£ π₯
finSupp β
} β¦ (( I βΎ Ο) β (π¦ β β‘((π§ β 2o, π€ β π β¦ ((2o
Β·o π€)
+o π§)) β
β‘(π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€))))))) β β‘(Ο CNF (π Β·o
2o))) |
12 | | eqid 2733 |
. 2
β’ (π₯ β (Ο
βo π),
π¦ β (Ο
βo π)
β¦ (((Ο βo π) Β·o π₯) +o π¦)) = (π₯ β (Ο βo π), π¦ β (Ο βo π) β¦ (((Ο
βo π)
Β·o π₯)
+o π¦)) |
13 | | eqid 2733 |
. 2
β’ (π₯ β π, π¦ β π β¦ β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©) = (π₯ β π, π¦ β π β¦ β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©) |
14 | | eqid 2733 |
. 2
β’ (β‘(πβπ) β ((((((Ο CNF π) β (π¦ β {π₯ β ((Ο βo
2o) βm π) β£ π₯ finSupp β
} β¦ (πΉ β (π¦ β β‘( I βΎ π))))) β β‘((Ο βo 2o)
CNF π)) β (((Ο
CNF (2o Β·o π)) β (π¦ β {π₯ β (Ο βm (π Β·o
2o)) β£ π₯
finSupp β
} β¦ (( I βΎ Ο) β (π¦ β β‘((π§ β 2o, π€ β π β¦ ((2o
Β·o π€)
+o π§)) β
β‘(π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€))))))) β β‘(Ο CNF (π Β·o 2o))))
β (π₯ β (Ο
βo π),
π¦ β (Ο
βo π)
β¦ (((Ο βo π) Β·o π₯) +o π¦))) β (π₯ β π, π¦ β π β¦ β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©))) = (β‘(πβπ) β ((((((Ο CNF π) β (π¦ β {π₯ β ((Ο βo
2o) βm π) β£ π₯ finSupp β
} β¦ (πΉ β (π¦ β β‘( I βΎ π))))) β β‘((Ο βo 2o)
CNF π)) β (((Ο
CNF (2o Β·o π)) β (π¦ β {π₯ β (Ο βm (π Β·o
2o)) β£ π₯
finSupp β
} β¦ (( I βΎ Ο) β (π¦ β β‘((π§ β 2o, π€ β π β¦ ((2o
Β·o π€)
+o π§)) β
β‘(π§ β 2o, π€ β π β¦ ((π Β·o π§) +o π€))))))) β β‘(Ο CNF (π Β·o 2o))))
β (π₯ β (Ο
βo π),
π¦ β (Ο
βo π)
β¦ (((Ο βo π) Β·o π₯) +o π¦))) β (π₯ β π, π¦ β π β¦ β¨((πβπ)βπ₯), ((πβπ)βπ¦)β©))) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | infxpenc2lem2 9961 |
1
β’ (π β βπβπ β π΄ (Ο β π β (πβπ):(π Γ π)β1-1-ontoβπ)) |