Step | Hyp | Ref
| Expression |
1 | | df-prod 15850 |
. 2
โข
โ๐ โ
๐ด ๐ต = (โฉ๐ฆ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ง(๐ง โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
2 | | nfcv 2904 |
. . . . 5
โข
โฒ๐ฅโค |
3 | | nfcprod.1 |
. . . . . . 7
โข
โฒ๐ฅ๐ด |
4 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฅ(โคโฅโ๐) |
5 | 3, 4 | nfss 3975 |
. . . . . 6
โข
โฒ๐ฅ ๐ด โ
(โคโฅโ๐) |
6 | | nfv 1918 |
. . . . . . . . 9
โข
โฒ๐ฅ ๐ง โ 0 |
7 | | nfcv 2904 |
. . . . . . . . . . 11
โข
โฒ๐ฅ๐ |
8 | | nfcv 2904 |
. . . . . . . . . . 11
โข
โฒ๐ฅ
ยท |
9 | 3 | nfcri 2891 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ ๐ โ ๐ด |
10 | | nfcprod.2 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ๐ต |
11 | | nfcv 2904 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ1 |
12 | 9, 10, 11 | nfif 4559 |
. . . . . . . . . . . 12
โข
โฒ๐ฅif(๐ โ ๐ด, ๐ต, 1) |
13 | 2, 12 | nfmpt 5256 |
. . . . . . . . . . 11
โข
โฒ๐ฅ(๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) |
14 | 7, 8, 13 | nfseq 13976 |
. . . . . . . . . 10
โข
โฒ๐ฅseq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) |
15 | | nfcv 2904 |
. . . . . . . . . 10
โข
โฒ๐ฅ
โ |
16 | | nfcv 2904 |
. . . . . . . . . 10
โข
โฒ๐ฅ๐ง |
17 | 14, 15, 16 | nfbr 5196 |
. . . . . . . . 9
โข
โฒ๐ฅseq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง |
18 | 6, 17 | nfan 1903 |
. . . . . . . 8
โข
โฒ๐ฅ(๐ง โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) |
19 | 18 | nfex 2318 |
. . . . . . 7
โข
โฒ๐ฅโ๐ง(๐ง โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) |
20 | 4, 19 | nfrexw 3311 |
. . . . . 6
โข
โฒ๐ฅโ๐ โ
(โคโฅโ๐)โ๐ง(๐ง โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) |
21 | | nfcv 2904 |
. . . . . . . 8
โข
โฒ๐ฅ๐ |
22 | 21, 8, 13 | nfseq 13976 |
. . . . . . 7
โข
โฒ๐ฅseq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) |
23 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฅ๐ฆ |
24 | 22, 15, 23 | nfbr 5196 |
. . . . . 6
โข
โฒ๐ฅseq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ |
25 | 5, 20, 24 | nf3an 1905 |
. . . . 5
โข
โฒ๐ฅ(๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ง(๐ง โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) |
26 | 2, 25 | nfrexw 3311 |
. . . 4
โข
โฒ๐ฅโ๐ โ โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ง(๐ง โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) |
27 | | nfcv 2904 |
. . . . 5
โข
โฒ๐ฅโ |
28 | | nfcv 2904 |
. . . . . . . 8
โข
โฒ๐ฅ๐ |
29 | | nfcv 2904 |
. . . . . . . 8
โข
โฒ๐ฅ(1...๐) |
30 | 28, 29, 3 | nff1o 6832 |
. . . . . . 7
โข
โฒ๐ฅ ๐:(1...๐)โ1-1-ontoโ๐ด |
31 | | nfcv 2904 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ(๐โ๐) |
32 | 31, 10 | nfcsbw 3921 |
. . . . . . . . . . 11
โข
โฒ๐ฅโฆ(๐โ๐) / ๐โฆ๐ต |
33 | 27, 32 | nfmpt 5256 |
. . . . . . . . . 10
โข
โฒ๐ฅ(๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) |
34 | 11, 8, 33 | nfseq 13976 |
. . . . . . . . 9
โข
โฒ๐ฅseq1(
ยท , (๐ โ
โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต)) |
35 | 34, 21 | nffv 6902 |
. . . . . . . 8
โข
โฒ๐ฅ(seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) |
36 | 35 | nfeq2 2921 |
. . . . . . 7
โข
โฒ๐ฅ ๐ฆ = (seq1( ยท , (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต))โ๐) |
37 | 30, 36 | nfan 1903 |
. . . . . 6
โข
โฒ๐ฅ(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) |
38 | 37 | nfex 2318 |
. . . . 5
โข
โฒ๐ฅโ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) |
39 | 27, 38 | nfrexw 3311 |
. . . 4
โข
โฒ๐ฅโ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)) |
40 | 26, 39 | nfor 1908 |
. . 3
โข
โฒ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ง(๐ง โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐))) |
41 | 40 | nfiotaw 6500 |
. 2
โข
โฒ๐ฅ(โฉ๐ฆ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ง(๐ง โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) |
42 | 1, 41 | nfcxfr 2902 |
1
โข
โฒ๐ฅโ๐ โ ๐ด ๐ต |