Step |
Hyp |
Ref |
Expression |
0 |
|
vk |
โข ๐ |
1 |
|
cA |
โข ๐ด |
2 |
|
cB |
โข ๐ต |
3 |
1 2 0
|
cprod |
โข โ ๐ โ ๐ด ๐ต |
4 |
|
vx |
โข ๐ฅ |
5 |
|
vm |
โข ๐ |
6 |
|
cz |
โข โค |
7 |
|
cuz |
โข โคโฅ |
8 |
5
|
cv |
โข ๐ |
9 |
8 7
|
cfv |
โข ( โคโฅ โ ๐ ) |
10 |
1 9
|
wss |
โข ๐ด โ ( โคโฅ โ ๐ ) |
11 |
|
vn |
โข ๐ |
12 |
|
vy |
โข ๐ฆ |
13 |
12
|
cv |
โข ๐ฆ |
14 |
|
cc0 |
โข 0 |
15 |
13 14
|
wne |
โข ๐ฆ โ 0 |
16 |
11
|
cv |
โข ๐ |
17 |
|
cmul |
โข ยท |
18 |
0
|
cv |
โข ๐ |
19 |
18 1
|
wcel |
โข ๐ โ ๐ด |
20 |
|
c1 |
โข 1 |
21 |
19 2 20
|
cif |
โข if ( ๐ โ ๐ด , ๐ต , 1 ) |
22 |
0 6 21
|
cmpt |
โข ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) |
23 |
17 22 16
|
cseq |
โข seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) |
24 |
|
cli |
โข โ |
25 |
23 13 24
|
wbr |
โข seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ |
26 |
15 25
|
wa |
โข ( ๐ฆ โ 0 โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ ) |
27 |
26 12
|
wex |
โข โ ๐ฆ ( ๐ฆ โ 0 โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ ) |
28 |
27 11 9
|
wrex |
โข โ ๐ โ ( โคโฅ โ ๐ ) โ ๐ฆ ( ๐ฆ โ 0 โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ ) |
29 |
17 22 8
|
cseq |
โข seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) |
30 |
4
|
cv |
โข ๐ฅ |
31 |
29 30 24
|
wbr |
โข seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฅ |
32 |
10 28 31
|
w3a |
โข ( ๐ด โ ( โคโฅ โ ๐ ) โง โ ๐ โ ( โคโฅ โ ๐ ) โ ๐ฆ ( ๐ฆ โ 0 โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ ) โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฅ ) |
33 |
32 5 6
|
wrex |
โข โ ๐ โ โค ( ๐ด โ ( โคโฅ โ ๐ ) โง โ ๐ โ ( โคโฅ โ ๐ ) โ ๐ฆ ( ๐ฆ โ 0 โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ ) โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฅ ) |
34 |
|
cn |
โข โ |
35 |
|
vf |
โข ๐ |
36 |
35
|
cv |
โข ๐ |
37 |
|
cfz |
โข ... |
38 |
20 8 37
|
co |
โข ( 1 ... ๐ ) |
39 |
38 1 36
|
wf1o |
โข ๐ : ( 1 ... ๐ ) โ1-1-ontoโ ๐ด |
40 |
16 36
|
cfv |
โข ( ๐ โ ๐ ) |
41 |
0 40 2
|
csb |
โข โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต |
42 |
11 34 41
|
cmpt |
โข ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) |
43 |
17 42 20
|
cseq |
โข seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) |
44 |
8 43
|
cfv |
โข ( seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) โ ๐ ) |
45 |
30 44
|
wceq |
โข ๐ฅ = ( seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) โ ๐ ) |
46 |
39 45
|
wa |
โข ( ๐ : ( 1 ... ๐ ) โ1-1-ontoโ ๐ด โง ๐ฅ = ( seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) โ ๐ ) ) |
47 |
46 35
|
wex |
โข โ ๐ ( ๐ : ( 1 ... ๐ ) โ1-1-ontoโ ๐ด โง ๐ฅ = ( seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) โ ๐ ) ) |
48 |
47 5 34
|
wrex |
โข โ ๐ โ โ โ ๐ ( ๐ : ( 1 ... ๐ ) โ1-1-ontoโ ๐ด โง ๐ฅ = ( seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) โ ๐ ) ) |
49 |
33 48
|
wo |
โข ( โ ๐ โ โค ( ๐ด โ ( โคโฅ โ ๐ ) โง โ ๐ โ ( โคโฅ โ ๐ ) โ ๐ฆ ( ๐ฆ โ 0 โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ ) โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฅ ) โจ โ ๐ โ โ โ ๐ ( ๐ : ( 1 ... ๐ ) โ1-1-ontoโ ๐ด โง ๐ฅ = ( seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) โ ๐ ) ) ) |
50 |
49 4
|
cio |
โข ( โฉ ๐ฅ ( โ ๐ โ โค ( ๐ด โ ( โคโฅ โ ๐ ) โง โ ๐ โ ( โคโฅ โ ๐ ) โ ๐ฆ ( ๐ฆ โ 0 โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ ) โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฅ ) โจ โ ๐ โ โ โ ๐ ( ๐ : ( 1 ... ๐ ) โ1-1-ontoโ ๐ด โง ๐ฅ = ( seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) โ ๐ ) ) ) ) |
51 |
3 50
|
wceq |
โข โ ๐ โ ๐ด ๐ต = ( โฉ ๐ฅ ( โ ๐ โ โค ( ๐ด โ ( โคโฅ โ ๐ ) โง โ ๐ โ ( โคโฅ โ ๐ ) โ ๐ฆ ( ๐ฆ โ 0 โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฆ ) โง seq ๐ ( ยท , ( ๐ โ โค โฆ if ( ๐ โ ๐ด , ๐ต , 1 ) ) ) โ ๐ฅ ) โจ โ ๐ โ โ โ ๐ ( ๐ : ( 1 ... ๐ ) โ1-1-ontoโ ๐ด โง ๐ฅ = ( seq 1 ( ยท , ( ๐ โ โ โฆ โฆ ( ๐ โ ๐ ) / ๐ โฆ ๐ต ) ) โ ๐ ) ) ) ) |