Step | Hyp | Ref
| Expression |
1 | | vdwmc.1 |
. . 3
โข ๐ โ V |
2 | | vdwmc.2 |
. . 3
โข (๐ โ ๐พ โ
โ0) |
3 | | vdwmc.3 |
. . 3
โข (๐ โ ๐น:๐โถ๐
) |
4 | 1, 2, 3 | vdwmc 16911 |
. 2
โข (๐ โ (๐พ MonoAP ๐น โ โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) |
5 | | vdwapid1 16908 |
. . . . . . . . . . . 12
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ ๐ โ (๐(APโ๐พ)๐)) |
6 | 5 | ne0d 4336 |
. . . . . . . . . . 11
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ (๐(APโ๐พ)๐) โ โ
) |
7 | 6 | 3expb 1121 |
. . . . . . . . . 10
โข ((๐พ โ โ โง (๐ โ โ โง ๐ โ โ)) โ (๐(APโ๐พ)๐) โ โ
) |
8 | 7 | adantll 713 |
. . . . . . . . 9
โข (((๐ โง ๐พ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐(APโ๐พ)๐) โ โ
) |
9 | | ssn0 4401 |
. . . . . . . . . 10
โข (((๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โง (๐(APโ๐พ)๐) โ โ
) โ (โก๐น โ {๐}) โ โ
) |
10 | 9 | expcom 415 |
. . . . . . . . 9
โข ((๐(APโ๐พ)๐) โ โ
โ ((๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ (โก๐น โ {๐}) โ โ
)) |
11 | 8, 10 | syl 17 |
. . . . . . . 8
โข (((๐ โง ๐พ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ (โก๐น โ {๐}) โ โ
)) |
12 | | disjsn 4716 |
. . . . . . . . . 10
โข ((๐
โฉ {๐}) = โ
โ ยฌ ๐ โ ๐
) |
13 | 3 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐พ โ โ) โ ๐น:๐โถ๐
) |
14 | | fimacnvdisj 6770 |
. . . . . . . . . . . . 13
โข ((๐น:๐โถ๐
โง (๐
โฉ {๐}) = โ
) โ (โก๐น โ {๐}) = โ
) |
15 | 14 | ex 414 |
. . . . . . . . . . . 12
โข (๐น:๐โถ๐
โ ((๐
โฉ {๐}) = โ
โ (โก๐น โ {๐}) = โ
)) |
16 | 13, 15 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐พ โ โ) โ ((๐
โฉ {๐}) = โ
โ (โก๐น โ {๐}) = โ
)) |
17 | 16 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐พ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐
โฉ {๐}) = โ
โ (โก๐น โ {๐}) = โ
)) |
18 | 12, 17 | biimtrrid 242 |
. . . . . . . . 9
โข (((๐ โง ๐พ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (ยฌ ๐ โ ๐
โ (โก๐น โ {๐}) = โ
)) |
19 | 18 | necon1ad 2958 |
. . . . . . . 8
โข (((๐ โง ๐พ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((โก๐น โ {๐}) โ โ
โ ๐ โ ๐
)) |
20 | 11, 19 | syld 47 |
. . . . . . 7
โข (((๐ โง ๐พ โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ ๐ โ ๐
)) |
21 | 20 | rexlimdvva 3212 |
. . . . . 6
โข ((๐ โง ๐พ โ โ) โ (โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ ๐ โ ๐
)) |
22 | 21 | pm4.71rd 564 |
. . . . 5
โข ((๐ โง ๐พ โ โ) โ (โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ (๐ โ ๐
โง โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})))) |
23 | 22 | exbidv 1925 |
. . . 4
โข ((๐ โง ๐พ โ โ) โ (โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐(๐ โ ๐
โง โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})))) |
24 | | df-rex 3072 |
. . . 4
โข
(โ๐ โ
๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐(๐ โ ๐
โง โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) |
25 | 23, 24 | bitr4di 289 |
. . 3
โข ((๐ โง ๐พ โ โ) โ (โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) |
26 | | vdwmc2.4 |
. . . . . . . 8
โข (๐ โ ๐ด โ ๐) |
27 | 3, 26 | ffvelcdmd 7088 |
. . . . . . 7
โข (๐ โ (๐นโ๐ด) โ ๐
) |
28 | 27 | ne0d 4336 |
. . . . . 6
โข (๐ โ ๐
โ โ
) |
29 | | 1nn 12223 |
. . . . . . . . 9
โข 1 โ
โ |
30 | 29 | ne0ii 4338 |
. . . . . . . 8
โข โ
โ โ
|
31 | | simpllr 775 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐พ = 0) โง ๐ โ โ) โง ๐ โ โ) โ ๐พ = 0) |
32 | 31 | fveq2d 6896 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐พ = 0) โง ๐ โ โ) โง ๐ โ โ) โ (APโ๐พ) =
(APโ0)) |
33 | 32 | oveqd 7426 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐พ = 0) โง ๐ โ โ) โง ๐ โ โ) โ (๐(APโ๐พ)๐) = (๐(APโ0)๐)) |
34 | | vdwap0 16909 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (๐(APโ0)๐) = โ
) |
35 | 34 | adantll 713 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐พ = 0) โง ๐ โ โ) โง ๐ โ โ) โ (๐(APโ0)๐) = โ
) |
36 | 33, 35 | eqtrd 2773 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐พ = 0) โง ๐ โ โ) โง ๐ โ โ) โ (๐(APโ๐พ)๐) = โ
) |
37 | | 0ss 4397 |
. . . . . . . . . . . 12
โข โ
โ (โก๐น โ {๐}) |
38 | 36, 37 | eqsstrdi 4037 |
. . . . . . . . . . 11
โข ((((๐ โง ๐พ = 0) โง ๐ โ โ) โง ๐ โ โ) โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
39 | 38 | ralrimiva 3147 |
. . . . . . . . . 10
โข (((๐ โง ๐พ = 0) โง ๐ โ โ) โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
40 | | r19.2z 4495 |
. . . . . . . . . 10
โข ((โ
โ โ
โง โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
41 | 30, 39, 40 | sylancr 588 |
. . . . . . . . 9
โข (((๐ โง ๐พ = 0) โง ๐ โ โ) โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
42 | 41 | ralrimiva 3147 |
. . . . . . . 8
โข ((๐ โง ๐พ = 0) โ โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
43 | | r19.2z 4495 |
. . . . . . . 8
โข ((โ
โ โ
โง โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) โ โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
44 | 30, 42, 43 | sylancr 588 |
. . . . . . 7
โข ((๐ โง ๐พ = 0) โ โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
45 | 44 | ralrimivw 3151 |
. . . . . 6
โข ((๐ โง ๐พ = 0) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
46 | | r19.2z 4495 |
. . . . . 6
โข ((๐
โ โ
โง
โ๐ โ ๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
47 | 28, 45, 46 | syl2an2r 684 |
. . . . 5
โข ((๐ โง ๐พ = 0) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
48 | | rexex 3077 |
. . . . 5
โข
(โ๐ โ
๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
49 | 47, 48 | syl 17 |
. . . 4
โข ((๐ โง ๐พ = 0) โ โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
50 | 49, 47 | 2thd 265 |
. . 3
โข ((๐ โง ๐พ = 0) โ (โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) |
51 | | elnn0 12474 |
. . . 4
โข (๐พ โ โ0
โ (๐พ โ โ
โจ ๐พ =
0)) |
52 | 2, 51 | sylib 217 |
. . 3
โข (๐ โ (๐พ โ โ โจ ๐พ = 0)) |
53 | 25, 50, 52 | mpjaodan 958 |
. 2
โข (๐ โ (โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) |
54 | | vdwapval 16906 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง ๐ โ โ
โง ๐ โ โ)
โ (๐ฅ โ (๐(APโ๐พ)๐) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ + (๐ ยท ๐)))) |
55 | 54 | 3expb 1121 |
. . . . . . . 8
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โ โ))
โ (๐ฅ โ (๐(APโ๐พ)๐) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ + (๐ ยท ๐)))) |
56 | 2, 55 | sylan 581 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐ฅ โ (๐(APโ๐พ)๐) โ โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ + (๐ ยท ๐)))) |
57 | 56 | imbi1d 342 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ฅ โ (๐(APโ๐พ)๐) โ ๐ฅ โ (โก๐น โ {๐})) โ (โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐})))) |
58 | 57 | albidv 1924 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (โ๐ฅ(๐ฅ โ (๐(APโ๐พ)๐) โ ๐ฅ โ (โก๐น โ {๐})) โ โ๐ฅ(โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐})))) |
59 | | dfss2 3969 |
. . . . 5
โข ((๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐ฅ(๐ฅ โ (๐(APโ๐พ)๐) โ ๐ฅ โ (โก๐น โ {๐}))) |
60 | | ralcom4 3284 |
. . . . . 6
โข
(โ๐ โ
(0...(๐พ โ
1))โ๐ฅ(๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐})) โ โ๐ฅโ๐ โ (0...(๐พ โ 1))(๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐}))) |
61 | | ovex 7442 |
. . . . . . . 8
โข (๐ + (๐ ยท ๐)) โ V |
62 | | eleq1 2822 |
. . . . . . . 8
โข (๐ฅ = (๐ + (๐ ยท ๐)) โ (๐ฅ โ (โก๐น โ {๐}) โ (๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |
63 | 61, 62 | ceqsalv 3512 |
. . . . . . 7
โข
(โ๐ฅ(๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐})) โ (๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
64 | 63 | ralbii 3094 |
. . . . . 6
โข
(โ๐ โ
(0...(๐พ โ
1))โ๐ฅ(๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐})) โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐})) |
65 | | r19.23v 3183 |
. . . . . . 7
โข
(โ๐ โ
(0...(๐พ โ 1))(๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐})) โ (โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐}))) |
66 | 65 | albii 1822 |
. . . . . 6
โข
(โ๐ฅโ๐ โ (0...(๐พ โ 1))(๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐})) โ โ๐ฅ(โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐}))) |
67 | 60, 64, 66 | 3bitr3i 301 |
. . . . 5
โข
(โ๐ โ
(0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}) โ โ๐ฅ(โ๐ โ (0...(๐พ โ 1))๐ฅ = (๐ + (๐ ยท ๐)) โ ๐ฅ โ (โก๐น โ {๐}))) |
68 | 58, 59, 67 | 3bitr4g 314 |
. . . 4
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |
69 | 68 | 2rexbidva 3218 |
. . 3
โข (๐ โ (โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |
70 | 69 | rexbidv 3179 |
. 2
โข (๐ โ (โ๐ โ ๐
โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |
71 | 4, 53, 70 | 3bitrd 305 |
1
โข (๐ โ (๐พ MonoAP ๐น โ โ๐ โ ๐
โ๐ โ โ โ๐ โ โ โ๐ โ (0...(๐พ โ 1))(๐ + (๐ ยท ๐)) โ (โก๐น โ {๐}))) |