Metamath Proof Explorer

Theorem infxpenc

Description: A canonical version of infxpen , by a completely different approach (although it uses infxpen via xpomen ). Using Cantor's normal form, we can show that A ^o B respects equinumerosity ( oef1o ), so that all the steps of (om ^ W ) x. ( om ^ W ) ~_om ^ ( 2 W ) ~ (om ^ 2 ) ^ W ~_om ^ W can be verified using bijections to do the ordinal commutations. (The assumption on N can be satisfied using cnfcom3c .) (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses infxpenc.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ On )
infxpenc.2 โŠข ( ๐œ‘ โ†’ ฯ‰ โŠ† ๐ด )
infxpenc.3 โŠข ( ๐œ‘ โ†’ ๐‘Š โˆˆ ( On โˆ– 1o ) )
infxpenc.4 โŠข ( ๐œ‘ โ†’ ๐น : ( ฯ‰ โ†‘o 2o ) โ€“1-1-ontoโ†’ ฯ‰ )
infxpenc.5 โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ โˆ… ) = โˆ… )
infxpenc.6 โŠข ( ๐œ‘ โ†’ ๐‘ : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
infxpenc.k โŠข ๐พ = ( ๐‘ฆ โˆˆ { ๐‘ฅ โˆˆ ( ( ฯ‰ โ†‘o 2o ) โ†‘m ๐‘Š ) โˆฃ ๐‘ฅ finSupp โˆ… } โ†ฆ ( ๐น โˆ˜ ( ๐‘ฆ โˆ˜ โ—ก ( I โ†พ ๐‘Š ) ) ) )
infxpenc.h โŠข ๐ป = ( ( ( ฯ‰ CNF ๐‘Š ) โˆ˜ ๐พ ) โˆ˜ โ—ก ( ( ฯ‰ โ†‘o 2o ) CNF ๐‘Š ) )
infxpenc.l โŠข ๐ฟ = ( ๐‘ฆ โˆˆ { ๐‘ฅ โˆˆ ( ฯ‰ โ†‘m ( ๐‘Š ยทo 2o ) ) โˆฃ ๐‘ฅ finSupp โˆ… } โ†ฆ ( ( I โ†พ ฯ‰ ) โˆ˜ ( ๐‘ฆ โˆ˜ โ—ก ( ๐‘Œ โˆ˜ โ—ก ๐‘‹ ) ) ) )
infxpenc.x โŠข ๐‘‹ = ( ๐‘ง โˆˆ 2o , ๐‘ค โˆˆ ๐‘Š โ†ฆ ( ( ๐‘Š ยทo ๐‘ง ) +o ๐‘ค ) )
infxpenc.y โŠข ๐‘Œ = ( ๐‘ง โˆˆ 2o , ๐‘ค โˆˆ ๐‘Š โ†ฆ ( ( 2o ยทo ๐‘ค ) +o ๐‘ง ) )
infxpenc.j โŠข ๐ฝ = ( ( ( ฯ‰ CNF ( 2o ยทo ๐‘Š ) ) โˆ˜ ๐ฟ ) โˆ˜ โ—ก ( ฯ‰ CNF ( ๐‘Š ยทo 2o ) ) )
infxpenc.z โŠข ๐‘ = ( ๐‘ฅ โˆˆ ( ฯ‰ โ†‘o ๐‘Š ) , ๐‘ฆ โˆˆ ( ฯ‰ โ†‘o ๐‘Š ) โ†ฆ ( ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ๐‘ฅ ) +o ๐‘ฆ ) )
infxpenc.t โŠข ๐‘‡ = ( ๐‘ฅ โˆˆ ๐ด , ๐‘ฆ โˆˆ ๐ด โ†ฆ โŸจ ( ๐‘ โ€˜ ๐‘ฅ ) , ( ๐‘ โ€˜ ๐‘ฆ ) โŸฉ )
infxpenc.g โŠข ๐บ = ( โ—ก ๐‘ โˆ˜ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) )
Assertion infxpenc ( ๐œ‘ โ†’ ๐บ : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ๐ด )

Proof

Step Hyp Ref Expression
1 infxpenc.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ On )
2 infxpenc.2 โŠข ( ๐œ‘ โ†’ ฯ‰ โŠ† ๐ด )
3 infxpenc.3 โŠข ( ๐œ‘ โ†’ ๐‘Š โˆˆ ( On โˆ– 1o ) )
4 infxpenc.4 โŠข ( ๐œ‘ โ†’ ๐น : ( ฯ‰ โ†‘o 2o ) โ€“1-1-ontoโ†’ ฯ‰ )
5 infxpenc.5 โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ โˆ… ) = โˆ… )
6 infxpenc.6 โŠข ( ๐œ‘ โ†’ ๐‘ : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
7 infxpenc.k โŠข ๐พ = ( ๐‘ฆ โˆˆ { ๐‘ฅ โˆˆ ( ( ฯ‰ โ†‘o 2o ) โ†‘m ๐‘Š ) โˆฃ ๐‘ฅ finSupp โˆ… } โ†ฆ ( ๐น โˆ˜ ( ๐‘ฆ โˆ˜ โ—ก ( I โ†พ ๐‘Š ) ) ) )
8 infxpenc.h โŠข ๐ป = ( ( ( ฯ‰ CNF ๐‘Š ) โˆ˜ ๐พ ) โˆ˜ โ—ก ( ( ฯ‰ โ†‘o 2o ) CNF ๐‘Š ) )
9 infxpenc.l โŠข ๐ฟ = ( ๐‘ฆ โˆˆ { ๐‘ฅ โˆˆ ( ฯ‰ โ†‘m ( ๐‘Š ยทo 2o ) ) โˆฃ ๐‘ฅ finSupp โˆ… } โ†ฆ ( ( I โ†พ ฯ‰ ) โˆ˜ ( ๐‘ฆ โˆ˜ โ—ก ( ๐‘Œ โˆ˜ โ—ก ๐‘‹ ) ) ) )
10 infxpenc.x โŠข ๐‘‹ = ( ๐‘ง โˆˆ 2o , ๐‘ค โˆˆ ๐‘Š โ†ฆ ( ( ๐‘Š ยทo ๐‘ง ) +o ๐‘ค ) )
11 infxpenc.y โŠข ๐‘Œ = ( ๐‘ง โˆˆ 2o , ๐‘ค โˆˆ ๐‘Š โ†ฆ ( ( 2o ยทo ๐‘ค ) +o ๐‘ง ) )
12 infxpenc.j โŠข ๐ฝ = ( ( ( ฯ‰ CNF ( 2o ยทo ๐‘Š ) ) โˆ˜ ๐ฟ ) โˆ˜ โ—ก ( ฯ‰ CNF ( ๐‘Š ยทo 2o ) ) )
13 infxpenc.z โŠข ๐‘ = ( ๐‘ฅ โˆˆ ( ฯ‰ โ†‘o ๐‘Š ) , ๐‘ฆ โˆˆ ( ฯ‰ โ†‘o ๐‘Š ) โ†ฆ ( ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ๐‘ฅ ) +o ๐‘ฆ ) )
14 infxpenc.t โŠข ๐‘‡ = ( ๐‘ฅ โˆˆ ๐ด , ๐‘ฆ โˆˆ ๐ด โ†ฆ โŸจ ( ๐‘ โ€˜ ๐‘ฅ ) , ( ๐‘ โ€˜ ๐‘ฆ ) โŸฉ )
15 infxpenc.g โŠข ๐บ = ( โ—ก ๐‘ โˆ˜ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) )
16 f1ocnv โŠข ( ๐‘ : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) โ†’ โ—ก ๐‘ : ( ฯ‰ โ†‘o ๐‘Š ) โ€“1-1-ontoโ†’ ๐ด )
17 6 16 syl โŠข ( ๐œ‘ โ†’ โ—ก ๐‘ : ( ฯ‰ โ†‘o ๐‘Š ) โ€“1-1-ontoโ†’ ๐ด )
18 f1oi โŠข ( I โ†พ ๐‘Š ) : ๐‘Š โ€“1-1-ontoโ†’ ๐‘Š
19 18 a1i โŠข ( ๐œ‘ โ†’ ( I โ†พ ๐‘Š ) : ๐‘Š โ€“1-1-ontoโ†’ ๐‘Š )
20 omelon โŠข ฯ‰ โˆˆ On
21 20 a1i โŠข ( ๐œ‘ โ†’ ฯ‰ โˆˆ On )
22 2on โŠข 2o โˆˆ On
23 oecl โŠข ( ( ฯ‰ โˆˆ On โˆง 2o โˆˆ On ) โ†’ ( ฯ‰ โ†‘o 2o ) โˆˆ On )
24 21 22 23 sylancl โŠข ( ๐œ‘ โ†’ ( ฯ‰ โ†‘o 2o ) โˆˆ On )
25 22 a1i โŠข ( ๐œ‘ โ†’ 2o โˆˆ On )
26 peano1 โŠข โˆ… โˆˆ ฯ‰
27 26 a1i โŠข ( ๐œ‘ โ†’ โˆ… โˆˆ ฯ‰ )
28 oen0 โŠข ( ( ( ฯ‰ โˆˆ On โˆง 2o โˆˆ On ) โˆง โˆ… โˆˆ ฯ‰ ) โ†’ โˆ… โˆˆ ( ฯ‰ โ†‘o 2o ) )
29 21 25 27 28 syl21anc โŠข ( ๐œ‘ โ†’ โˆ… โˆˆ ( ฯ‰ โ†‘o 2o ) )
30 ondif1 โŠข ( ( ฯ‰ โ†‘o 2o ) โˆˆ ( On โˆ– 1o ) โ†” ( ( ฯ‰ โ†‘o 2o ) โˆˆ On โˆง โˆ… โˆˆ ( ฯ‰ โ†‘o 2o ) ) )
31 24 29 30 sylanbrc โŠข ( ๐œ‘ โ†’ ( ฯ‰ โ†‘o 2o ) โˆˆ ( On โˆ– 1o ) )
32 3 eldifad โŠข ( ๐œ‘ โ†’ ๐‘Š โˆˆ On )
33 4 19 31 32 21 32 5 7 8 oef1o โŠข ( ๐œ‘ โ†’ ๐ป : ( ( ฯ‰ โ†‘o 2o ) โ†‘o ๐‘Š ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
34 f1oi โŠข ( I โ†พ ฯ‰ ) : ฯ‰ โ€“1-1-ontoโ†’ ฯ‰
35 34 a1i โŠข ( ๐œ‘ โ†’ ( I โ†พ ฯ‰ ) : ฯ‰ โ€“1-1-ontoโ†’ ฯ‰ )
36 10 11 omf1o โŠข ( ( ๐‘Š โˆˆ On โˆง 2o โˆˆ On ) โ†’ ( ๐‘Œ โˆ˜ โ—ก ๐‘‹ ) : ( ๐‘Š ยทo 2o ) โ€“1-1-ontoโ†’ ( 2o ยทo ๐‘Š ) )
37 32 22 36 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘Œ โˆ˜ โ—ก ๐‘‹ ) : ( ๐‘Š ยทo 2o ) โ€“1-1-ontoโ†’ ( 2o ยทo ๐‘Š ) )
38 ondif1 โŠข ( ฯ‰ โˆˆ ( On โˆ– 1o ) โ†” ( ฯ‰ โˆˆ On โˆง โˆ… โˆˆ ฯ‰ ) )
39 20 26 38 mpbir2an โŠข ฯ‰ โˆˆ ( On โˆ– 1o )
40 39 a1i โŠข ( ๐œ‘ โ†’ ฯ‰ โˆˆ ( On โˆ– 1o ) )
41 omcl โŠข ( ( ๐‘Š โˆˆ On โˆง 2o โˆˆ On ) โ†’ ( ๐‘Š ยทo 2o ) โˆˆ On )
42 32 22 41 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘Š ยทo 2o ) โˆˆ On )
43 omcl โŠข ( ( 2o โˆˆ On โˆง ๐‘Š โˆˆ On ) โ†’ ( 2o ยทo ๐‘Š ) โˆˆ On )
44 25 32 43 syl2anc โŠข ( ๐œ‘ โ†’ ( 2o ยทo ๐‘Š ) โˆˆ On )
45 fvresi โŠข ( โˆ… โˆˆ ฯ‰ โ†’ ( ( I โ†พ ฯ‰ ) โ€˜ โˆ… ) = โˆ… )
46 26 45 mp1i โŠข ( ๐œ‘ โ†’ ( ( I โ†พ ฯ‰ ) โ€˜ โˆ… ) = โˆ… )
47 35 37 40 42 21 44 46 9 12 oef1o โŠข ( ๐œ‘ โ†’ ๐ฝ : ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ( 2o ยทo ๐‘Š ) ) )
48 oeoe โŠข ( ( ฯ‰ โˆˆ On โˆง 2o โˆˆ On โˆง ๐‘Š โˆˆ On ) โ†’ ( ( ฯ‰ โ†‘o 2o ) โ†‘o ๐‘Š ) = ( ฯ‰ โ†‘o ( 2o ยทo ๐‘Š ) ) )
49 20 25 32 48 mp3an2i โŠข ( ๐œ‘ โ†’ ( ( ฯ‰ โ†‘o 2o ) โ†‘o ๐‘Š ) = ( ฯ‰ โ†‘o ( 2o ยทo ๐‘Š ) ) )
50 49 f1oeq3d โŠข ( ๐œ‘ โ†’ ( ๐ฝ : ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o 2o ) โ†‘o ๐‘Š ) โ†” ๐ฝ : ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ( 2o ยทo ๐‘Š ) ) ) )
51 47 50 mpbird โŠข ( ๐œ‘ โ†’ ๐ฝ : ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o 2o ) โ†‘o ๐‘Š ) )
52 f1oco โŠข ( ( ๐ป : ( ( ฯ‰ โ†‘o 2o ) โ†‘o ๐‘Š ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) โˆง ๐ฝ : ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o 2o ) โ†‘o ๐‘Š ) ) โ†’ ( ๐ป โˆ˜ ๐ฝ ) : ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
53 33 51 52 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐ป โˆ˜ ๐ฝ ) : ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
54 df-2o โŠข 2o = suc 1o
55 54 oveq2i โŠข ( ๐‘Š ยทo 2o ) = ( ๐‘Š ยทo suc 1o )
56 1on โŠข 1o โˆˆ On
57 omsuc โŠข ( ( ๐‘Š โˆˆ On โˆง 1o โˆˆ On ) โ†’ ( ๐‘Š ยทo suc 1o ) = ( ( ๐‘Š ยทo 1o ) +o ๐‘Š ) )
58 32 56 57 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘Š ยทo suc 1o ) = ( ( ๐‘Š ยทo 1o ) +o ๐‘Š ) )
59 55 58 eqtrid โŠข ( ๐œ‘ โ†’ ( ๐‘Š ยทo 2o ) = ( ( ๐‘Š ยทo 1o ) +o ๐‘Š ) )
60 om1 โŠข ( ๐‘Š โˆˆ On โ†’ ( ๐‘Š ยทo 1o ) = ๐‘Š )
61 32 60 syl โŠข ( ๐œ‘ โ†’ ( ๐‘Š ยทo 1o ) = ๐‘Š )
62 61 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ๐‘Š ยทo 1o ) +o ๐‘Š ) = ( ๐‘Š +o ๐‘Š ) )
63 59 62 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐‘Š ยทo 2o ) = ( ๐‘Š +o ๐‘Š ) )
64 63 oveq2d โŠข ( ๐œ‘ โ†’ ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) = ( ฯ‰ โ†‘o ( ๐‘Š +o ๐‘Š ) ) )
65 oeoa โŠข ( ( ฯ‰ โˆˆ On โˆง ๐‘Š โˆˆ On โˆง ๐‘Š โˆˆ On ) โ†’ ( ฯ‰ โ†‘o ( ๐‘Š +o ๐‘Š ) ) = ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) )
66 20 32 32 65 mp3an2i โŠข ( ๐œ‘ โ†’ ( ฯ‰ โ†‘o ( ๐‘Š +o ๐‘Š ) ) = ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) )
67 64 66 eqtrd โŠข ( ๐œ‘ โ†’ ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) = ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) )
68 67 f1oeq2d โŠข ( ๐œ‘ โ†’ ( ( ๐ป โˆ˜ ๐ฝ ) : ( ฯ‰ โ†‘o ( ๐‘Š ยทo 2o ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) โ†” ( ๐ป โˆ˜ ๐ฝ ) : ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) ) )
69 53 68 mpbid โŠข ( ๐œ‘ โ†’ ( ๐ป โˆ˜ ๐ฝ ) : ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
70 oecl โŠข ( ( ฯ‰ โˆˆ On โˆง ๐‘Š โˆˆ On ) โ†’ ( ฯ‰ โ†‘o ๐‘Š ) โˆˆ On )
71 21 32 70 syl2anc โŠข ( ๐œ‘ โ†’ ( ฯ‰ โ†‘o ๐‘Š ) โˆˆ On )
72 13 omxpenlem โŠข ( ( ( ฯ‰ โ†‘o ๐‘Š ) โˆˆ On โˆง ( ฯ‰ โ†‘o ๐‘Š ) โˆˆ On ) โ†’ ๐‘ : ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) )
73 71 71 72 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘ : ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) )
74 f1oco โŠข ( ( ( ๐ป โˆ˜ ๐ฝ ) : ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) โˆง ๐‘ : ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ยทo ( ฯ‰ โ†‘o ๐‘Š ) ) ) โ†’ ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) : ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
75 69 73 74 syl2anc โŠข ( ๐œ‘ โ†’ ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) : ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
76 f1of โŠข ( ๐‘ : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) โ†’ ๐‘ : ๐ด โŸถ ( ฯ‰ โ†‘o ๐‘Š ) )
77 6 76 syl โŠข ( ๐œ‘ โ†’ ๐‘ : ๐ด โŸถ ( ฯ‰ โ†‘o ๐‘Š ) )
78 77 feqmptd โŠข ( ๐œ‘ โ†’ ๐‘ = ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ( ๐‘ โ€˜ ๐‘ฅ ) ) )
79 78 f1oeq1d โŠข ( ๐œ‘ โ†’ ( ๐‘ : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) โ†” ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ( ๐‘ โ€˜ ๐‘ฅ ) ) : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) ) )
80 6 79 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ( ๐‘ โ€˜ ๐‘ฅ ) ) : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
81 77 feqmptd โŠข ( ๐œ‘ โ†’ ๐‘ = ( ๐‘ฆ โˆˆ ๐ด โ†ฆ ( ๐‘ โ€˜ ๐‘ฆ ) ) )
82 81 f1oeq1d โŠข ( ๐œ‘ โ†’ ( ๐‘ : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) โ†” ( ๐‘ฆ โˆˆ ๐ด โ†ฆ ( ๐‘ โ€˜ ๐‘ฆ ) ) : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) ) )
83 6 82 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘ฆ โˆˆ ๐ด โ†ฆ ( ๐‘ โ€˜ ๐‘ฆ ) ) : ๐ด โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
84 80 83 xpf1o โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ด , ๐‘ฆ โˆˆ ๐ด โ†ฆ โŸจ ( ๐‘ โ€˜ ๐‘ฅ ) , ( ๐‘ โ€˜ ๐‘ฆ ) โŸฉ ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) )
85 f1oeq1 โŠข ( ๐‘‡ = ( ๐‘ฅ โˆˆ ๐ด , ๐‘ฆ โˆˆ ๐ด โ†ฆ โŸจ ( ๐‘ โ€˜ ๐‘ฅ ) , ( ๐‘ โ€˜ ๐‘ฆ ) โŸฉ ) โ†’ ( ๐‘‡ : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) โ†” ( ๐‘ฅ โˆˆ ๐ด , ๐‘ฆ โˆˆ ๐ด โ†ฆ โŸจ ( ๐‘ โ€˜ ๐‘ฅ ) , ( ๐‘ โ€˜ ๐‘ฆ ) โŸฉ ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) ) )
86 14 85 ax-mp โŠข ( ๐‘‡ : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) โ†” ( ๐‘ฅ โˆˆ ๐ด , ๐‘ฆ โˆˆ ๐ด โ†ฆ โŸจ ( ๐‘ โ€˜ ๐‘ฅ ) , ( ๐‘ โ€˜ ๐‘ฆ ) โŸฉ ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) )
87 84 86 sylibr โŠข ( ๐œ‘ โ†’ ๐‘‡ : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) )
88 f1oco โŠข ( ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) : ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) โˆง ๐‘‡ : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ( ฯ‰ โ†‘o ๐‘Š ) ร— ( ฯ‰ โ†‘o ๐‘Š ) ) ) โ†’ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
89 75 87 88 syl2anc โŠข ( ๐œ‘ โ†’ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) )
90 f1oco โŠข ( ( โ—ก ๐‘ : ( ฯ‰ โ†‘o ๐‘Š ) โ€“1-1-ontoโ†’ ๐ด โˆง ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ( ฯ‰ โ†‘o ๐‘Š ) ) โ†’ ( โ—ก ๐‘ โˆ˜ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ๐ด )
91 17 89 90 syl2anc โŠข ( ๐œ‘ โ†’ ( โ—ก ๐‘ โˆ˜ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ๐ด )
92 f1oeq1 โŠข ( ๐บ = ( โ—ก ๐‘ โˆ˜ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) ) โ†’ ( ๐บ : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ๐ด โ†” ( โ—ก ๐‘ โˆ˜ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ๐ด ) )
93 15 92 ax-mp โŠข ( ๐บ : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ๐ด โ†” ( โ—ก ๐‘ โˆ˜ ( ( ( ๐ป โˆ˜ ๐ฝ ) โˆ˜ ๐‘ ) โˆ˜ ๐‘‡ ) ) : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ๐ด )
94 91 93 sylibr โŠข ( ๐œ‘ โ†’ ๐บ : ( ๐ด ร— ๐ด ) โ€“1-1-ontoโ†’ ๐ด )