Step | Hyp | Ref
| Expression |
1 | | df-proddc 11558 |
. 2
โข
โ๐ โ
๐ด ๐ต = (โฉ๐ฆ(โ๐ โ โค ((๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)DECID ๐ โ ๐ด) โง (โ๐ โ (โคโฅโ๐)โ๐ง(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)))โ๐)))) |
2 | | nfcv 2319 |
. . . . 5
โข
โฒ๐ฅโค |
3 | | nfcprod.1 |
. . . . . . . 8
โข
โฒ๐ฅ๐ด |
4 | | nfcv 2319 |
. . . . . . . 8
โข
โฒ๐ฅ(โคโฅโ๐) |
5 | 3, 4 | nfss 3148 |
. . . . . . 7
โข
โฒ๐ฅ ๐ด โ
(โคโฅโ๐) |
6 | 3 | nfcri 2313 |
. . . . . . . . 9
โข
โฒ๐ฅ ๐ โ ๐ด |
7 | 6 | nfdc 1659 |
. . . . . . . 8
โข
โฒ๐ฅDECID ๐ โ ๐ด |
8 | 4, 7 | nfralxy 2515 |
. . . . . . 7
โข
โฒ๐ฅโ๐ โ (โคโฅโ๐)DECID ๐ โ ๐ด |
9 | 5, 8 | nfan 1565 |
. . . . . 6
โข
โฒ๐ฅ(๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)DECID ๐ โ ๐ด) |
10 | | nfv 1528 |
. . . . . . . . . 10
โข
โฒ๐ฅ ๐ง # 0 |
11 | | nfcv 2319 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ๐ |
12 | | nfcv 2319 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ
ยท |
13 | 3 | nfcri 2313 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅ ๐ โ ๐ด |
14 | | nfcprod.2 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅ๐ต |
15 | | nfcv 2319 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅ1 |
16 | 13, 14, 15 | nfif 3562 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅif(๐ โ ๐ด, ๐ต, 1) |
17 | 2, 16 | nfmpt 4095 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ(๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) |
18 | 11, 12, 17 | nfseq 10454 |
. . . . . . . . . . 11
โข
โฒ๐ฅseq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) |
19 | | nfcv 2319 |
. . . . . . . . . . 11
โข
โฒ๐ฅ
โ |
20 | | nfcv 2319 |
. . . . . . . . . . 11
โข
โฒ๐ฅ๐ง |
21 | 18, 19, 20 | nfbr 4049 |
. . . . . . . . . 10
โข
โฒ๐ฅseq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง |
22 | 10, 21 | nfan 1565 |
. . . . . . . . 9
โข
โฒ๐ฅ(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) |
23 | 22 | nfex 1637 |
. . . . . . . 8
โข
โฒ๐ฅโ๐ง(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) |
24 | 4, 23 | nfrexxy 2516 |
. . . . . . 7
โข
โฒ๐ฅโ๐ โ
(โคโฅโ๐)โ๐ง(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) |
25 | | nfcv 2319 |
. . . . . . . . 9
โข
โฒ๐ฅ๐ |
26 | 25, 12, 17 | nfseq 10454 |
. . . . . . . 8
โข
โฒ๐ฅseq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) |
27 | | nfcv 2319 |
. . . . . . . 8
โข
โฒ๐ฅ๐ฆ |
28 | 26, 19, 27 | nfbr 4049 |
. . . . . . 7
โข
โฒ๐ฅseq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ |
29 | 24, 28 | nfan 1565 |
. . . . . 6
โข
โฒ๐ฅ(โ๐ โ (โคโฅโ๐)โ๐ง(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) |
30 | 9, 29 | nfan 1565 |
. . . . 5
โข
โฒ๐ฅ((๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)DECID ๐ โ ๐ด) โง (โ๐ โ (โคโฅโ๐)โ๐ง(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) |
31 | 2, 30 | nfrexxy 2516 |
. . . 4
โข
โฒ๐ฅโ๐ โ โค ((๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)DECID ๐ โ ๐ด) โง (โ๐ โ (โคโฅโ๐)โ๐ง(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) |
32 | | nfcv 2319 |
. . . . 5
โข
โฒ๐ฅโ |
33 | | nfcv 2319 |
. . . . . . . 8
โข
โฒ๐ฅ๐ |
34 | | nfcv 2319 |
. . . . . . . 8
โข
โฒ๐ฅ(1...๐) |
35 | 33, 34, 3 | nff1o 5459 |
. . . . . . 7
โข
โฒ๐ฅ ๐:(1...๐)โ1-1-ontoโ๐ด |
36 | | nfv 1528 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ ๐ โค ๐ |
37 | | nfcv 2319 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ(๐โ๐) |
38 | 37, 14 | nfcsb 3094 |
. . . . . . . . . . . 12
โข
โฒ๐ฅโฆ(๐โ๐) / ๐โฆ๐ต |
39 | 36, 38, 15 | nfif 3562 |
. . . . . . . . . . 11
โข
โฒ๐ฅif(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1) |
40 | 32, 39 | nfmpt 4095 |
. . . . . . . . . 10
โข
โฒ๐ฅ(๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)) |
41 | 15, 12, 40 | nfseq 10454 |
. . . . . . . . 9
โข
โฒ๐ฅseq1(
ยท , (๐ โ
โ โฆ if(๐ โค
๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1))) |
42 | 41, 25 | nffv 5525 |
. . . . . . . 8
โข
โฒ๐ฅ(seq1( ยท , (๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)))โ๐) |
43 | 42 | nfeq2 2331 |
. . . . . . 7
โข
โฒ๐ฅ ๐ฆ = (seq1( ยท , (๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)))โ๐) |
44 | 35, 43 | nfan 1565 |
. . . . . 6
โข
โฒ๐ฅ(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)))โ๐)) |
45 | 44 | nfex 1637 |
. . . . 5
โข
โฒ๐ฅโ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)))โ๐)) |
46 | 32, 45 | nfrexxy 2516 |
. . . 4
โข
โฒ๐ฅโ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)))โ๐)) |
47 | 31, 46 | nfor 1574 |
. . 3
โข
โฒ๐ฅ(โ๐ โ โค ((๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)DECID ๐ โ ๐ด) โง (โ๐ โ (โคโฅโ๐)โ๐ง(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)))โ๐))) |
48 | 47 | nfiotaw 5182 |
. 2
โข
โฒ๐ฅ(โฉ๐ฆ(โ๐ โ โค ((๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)DECID ๐ โ ๐ด) โง (โ๐ โ (โคโฅโ๐)โ๐ง(๐ง # 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ง) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฆ = (seq1( ยท , (๐ โ โ โฆ if(๐ โค ๐, โฆ(๐โ๐) / ๐โฆ๐ต, 1)))โ๐)))) |
49 | 1, 48 | nfcxfr 2316 |
1
โข
โฒ๐ฅโ๐ โ ๐ด ๐ต |