Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
โข (๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) = (๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) |
2 | 1 | omxpenlem 9024 |
. . . . 5
โข ((๐ต โ On โง ๐ด โ On) โ (๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)):(๐ด ร ๐ต)โ1-1-ontoโ(๐ต ยทo ๐ด)) |
3 | 2 | ancoms 460 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ (๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)):(๐ด ร ๐ต)โ1-1-ontoโ(๐ต ยทo ๐ด)) |
4 | | eqid 2737 |
. . . . 5
โข (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง}) = (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง}) |
5 | 4 | xpcomf1o 9012 |
. . . 4
โข (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง}):(๐ต ร ๐ด)โ1-1-ontoโ(๐ด ร ๐ต) |
6 | | f1oco 6812 |
. . . 4
โข (((๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)):(๐ด ร ๐ต)โ1-1-ontoโ(๐ต ยทo ๐ด) โง (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง}):(๐ต ร ๐ด)โ1-1-ontoโ(๐ด ร ๐ต)) โ ((๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) โ (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง})):(๐ต ร ๐ด)โ1-1-ontoโ(๐ต ยทo ๐ด)) |
7 | 3, 5, 6 | sylancl 587 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) โ (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง})):(๐ต ร ๐ด)โ1-1-ontoโ(๐ต ยทo ๐ด)) |
8 | | omf1o.2 |
. . . . 5
โข ๐บ = (๐ฅ โ ๐ต, ๐ฆ โ ๐ด โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) |
9 | 4, 1 | xpcomco 9013 |
. . . . 5
โข ((๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) โ (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง})) = (๐ฅ โ ๐ต, ๐ฆ โ ๐ด โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) |
10 | 8, 9 | eqtr4i 2768 |
. . . 4
โข ๐บ = ((๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) โ (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง})) |
11 | | f1oeq1 6777 |
. . . 4
โข (๐บ = ((๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) โ (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง})) โ (๐บ:(๐ต ร ๐ด)โ1-1-ontoโ(๐ต ยทo ๐ด) โ ((๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) โ (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง})):(๐ต ร ๐ด)โ1-1-ontoโ(๐ต ยทo ๐ด))) |
12 | 10, 11 | ax-mp 5 |
. . 3
โข (๐บ:(๐ต ร ๐ด)โ1-1-ontoโ(๐ต ยทo ๐ด) โ ((๐ฆ โ ๐ด, ๐ฅ โ ๐ต โฆ ((๐ต ยทo ๐ฆ) +o ๐ฅ)) โ (๐ง โ (๐ต ร ๐ด) โฆ โช โก{๐ง})):(๐ต ร ๐ด)โ1-1-ontoโ(๐ต ยทo ๐ด)) |
13 | 7, 12 | sylibr 233 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ ๐บ:(๐ต ร ๐ด)โ1-1-ontoโ(๐ต ยทo ๐ด)) |
14 | | omf1o.1 |
. . . 4
โข ๐น = (๐ฅ โ ๐ต, ๐ฆ โ ๐ด โฆ ((๐ด ยทo ๐ฅ) +o ๐ฆ)) |
15 | 14 | omxpenlem 9024 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ ๐น:(๐ต ร ๐ด)โ1-1-ontoโ(๐ด ยทo ๐ต)) |
16 | | f1ocnv 6801 |
. . 3
โข (๐น:(๐ต ร ๐ด)โ1-1-ontoโ(๐ด ยทo ๐ต) โ โก๐น:(๐ด ยทo ๐ต)โ1-1-ontoโ(๐ต ร ๐ด)) |
17 | 15, 16 | syl 17 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ โก๐น:(๐ด ยทo ๐ต)โ1-1-ontoโ(๐ต ร ๐ด)) |
18 | | f1oco 6812 |
. 2
โข ((๐บ:(๐ต ร ๐ด)โ1-1-ontoโ(๐ต ยทo ๐ด) โง โก๐น:(๐ด ยทo ๐ต)โ1-1-ontoโ(๐ต ร ๐ด)) โ (๐บ โ โก๐น):(๐ด ยทo ๐ต)โ1-1-ontoโ(๐ต ยทo ๐ด)) |
19 | 13, 17, 18 | syl2anc 585 |
1
โข ((๐ด โ On โง ๐ต โ On) โ (๐บ โ โก๐น):(๐ด ยทo ๐ต)โ1-1-ontoโ(๐ต ยทo ๐ด)) |