Step | Hyp | Ref
| Expression |
1 | | isthincd2lem2.6 |
. . . 4
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง)) |
2 | | oveq1 7384 |
. . . . . 6
โข (๐ฅ = ๐ค โ (๐ฅ๐ป๐ฆ) = (๐ค๐ป๐ฆ)) |
3 | | opeq1 4850 |
. . . . . . . . . 10
โข (๐ฅ = ๐ค โ โจ๐ฅ, ๐ฆโฉ = โจ๐ค, ๐ฆโฉ) |
4 | 3 | oveq1d 7392 |
. . . . . . . . 9
โข (๐ฅ = ๐ค โ (โจ๐ฅ, ๐ฆโฉ ยท ๐ง) = (โจ๐ค, ๐ฆโฉ ยท ๐ง)) |
5 | 4 | oveqd 7394 |
. . . . . . . 8
โข (๐ฅ = ๐ค โ (๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ค, ๐ฆโฉ ยท ๐ง)๐)) |
6 | | oveq1 7384 |
. . . . . . . 8
โข (๐ฅ = ๐ค โ (๐ฅ๐ป๐ง) = (๐ค๐ป๐ง)) |
7 | 5, 6 | eleq12d 2826 |
. . . . . . 7
โข (๐ฅ = ๐ค โ ((๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โ (๐(โจ๐ค, ๐ฆโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง))) |
8 | 7 | ralbidv 3176 |
. . . . . 6
โข (๐ฅ = ๐ค โ (โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โ โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ค, ๐ฆโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง))) |
9 | 2, 8 | raleqbidv 3330 |
. . . . 5
โข (๐ฅ = ๐ค โ (โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โ โ๐ โ (๐ค๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ค, ๐ฆโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง))) |
10 | | oveq2 7385 |
. . . . . 6
โข (๐ฆ = ๐ฃ โ (๐ค๐ป๐ฆ) = (๐ค๐ป๐ฃ)) |
11 | | oveq1 7384 |
. . . . . . 7
โข (๐ฆ = ๐ฃ โ (๐ฆ๐ป๐ง) = (๐ฃ๐ป๐ง)) |
12 | | opeq2 4851 |
. . . . . . . . . 10
โข (๐ฆ = ๐ฃ โ โจ๐ค, ๐ฆโฉ = โจ๐ค, ๐ฃโฉ) |
13 | 12 | oveq1d 7392 |
. . . . . . . . 9
โข (๐ฆ = ๐ฃ โ (โจ๐ค, ๐ฆโฉ ยท ๐ง) = (โจ๐ค, ๐ฃโฉ ยท ๐ง)) |
14 | 13 | oveqd 7394 |
. . . . . . . 8
โข (๐ฆ = ๐ฃ โ (๐(โจ๐ค, ๐ฆโฉ ยท ๐ง)๐) = (๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐)) |
15 | 14 | eleq1d 2817 |
. . . . . . 7
โข (๐ฆ = ๐ฃ โ ((๐(โจ๐ค, ๐ฆโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง) โ (๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง))) |
16 | 11, 15 | raleqbidv 3330 |
. . . . . 6
โข (๐ฆ = ๐ฃ โ (โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ค, ๐ฆโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง) โ โ๐ โ (๐ฃ๐ป๐ง)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง))) |
17 | 10, 16 | raleqbidv 3330 |
. . . . 5
โข (๐ฆ = ๐ฃ โ (โ๐ โ (๐ค๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ค, ๐ฆโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง) โ โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ง)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง))) |
18 | | oveq2 7385 |
. . . . . . . 8
โข (๐ง = ๐ข โ (๐ฃ๐ป๐ง) = (๐ฃ๐ป๐ข)) |
19 | | oveq2 7385 |
. . . . . . . . . 10
โข (๐ง = ๐ข โ (โจ๐ค, ๐ฃโฉ ยท ๐ง) = (โจ๐ค, ๐ฃโฉ ยท ๐ข)) |
20 | 19 | oveqd 7394 |
. . . . . . . . 9
โข (๐ง = ๐ข โ (๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐) = (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐)) |
21 | | oveq2 7385 |
. . . . . . . . 9
โข (๐ง = ๐ข โ (๐ค๐ป๐ง) = (๐ค๐ป๐ข)) |
22 | 20, 21 | eleq12d 2826 |
. . . . . . . 8
โข (๐ง = ๐ข โ ((๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง) โ (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข))) |
23 | 18, 22 | raleqbidv 3330 |
. . . . . . 7
โข (๐ง = ๐ข โ (โ๐ โ (๐ฃ๐ป๐ง)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง) โ โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข))) |
24 | 23 | ralbidv 3176 |
. . . . . 6
โข (๐ง = ๐ข โ (โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ง)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง) โ โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข))) |
25 | | oveq2 7385 |
. . . . . . . 8
โข (๐ = ๐ โ (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) = (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐)) |
26 | 25 | eleq1d 2817 |
. . . . . . 7
โข (๐ = ๐ โ ((๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข) โ (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข))) |
27 | | oveq1 7384 |
. . . . . . . 8
โข (๐ = ๐ โ (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) = (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐)) |
28 | 27 | eleq1d 2817 |
. . . . . . 7
โข (๐ = ๐ โ ((๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข) โ (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข))) |
29 | 26, 28 | cbvral2vw 3235 |
. . . . . 6
โข
(โ๐ โ
(๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข) โ โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข)) |
30 | 24, 29 | bitrdi 286 |
. . . . 5
โข (๐ง = ๐ข โ (โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ง)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ง)๐) โ (๐ค๐ป๐ง) โ โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข))) |
31 | 9, 17, 30 | cbvral3vw 3237 |
. . . 4
โข
(โ๐ฅ โ
๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ โ (๐ฅ๐ป๐ฆ)โ๐ โ (๐ฆ๐ป๐ง)(๐(โจ๐ฅ, ๐ฆโฉ ยท ๐ง)๐) โ (๐ฅ๐ป๐ง) โ โ๐ค โ ๐ต โ๐ฃ โ ๐ต โ๐ข โ ๐ต โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข)) |
32 | 1, 31 | sylib 217 |
. . 3
โข (๐ โ โ๐ค โ ๐ต โ๐ฃ โ ๐ต โ๐ข โ ๐ต โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข)) |
33 | | isthincd2lem2.1 |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
34 | | isthincd2lem2.2 |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
35 | | isthincd2lem2.3 |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
36 | | oveq1 7384 |
. . . . . 6
โข (๐ค = ๐ โ (๐ค๐ป๐ฃ) = (๐๐ป๐ฃ)) |
37 | | opeq1 4850 |
. . . . . . . . . 10
โข (๐ค = ๐ โ โจ๐ค, ๐ฃโฉ = โจ๐, ๐ฃโฉ) |
38 | 37 | oveq1d 7392 |
. . . . . . . . 9
โข (๐ค = ๐ โ (โจ๐ค, ๐ฃโฉ ยท ๐ข) = (โจ๐, ๐ฃโฉ ยท ๐ข)) |
39 | 38 | oveqd 7394 |
. . . . . . . 8
โข (๐ค = ๐ โ (๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) = (๐(โจ๐, ๐ฃโฉ ยท ๐ข)๐)) |
40 | | oveq1 7384 |
. . . . . . . 8
โข (๐ค = ๐ โ (๐ค๐ป๐ข) = (๐๐ป๐ข)) |
41 | 39, 40 | eleq12d 2826 |
. . . . . . 7
โข (๐ค = ๐ โ ((๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข) โ (๐(โจ๐, ๐ฃโฉ ยท ๐ข)๐) โ (๐๐ป๐ข))) |
42 | 41 | ralbidv 3176 |
. . . . . 6
โข (๐ค = ๐ โ (โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข) โ โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐, ๐ฃโฉ ยท ๐ข)๐) โ (๐๐ป๐ข))) |
43 | 36, 42 | raleqbidv 3330 |
. . . . 5
โข (๐ค = ๐ โ (โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข) โ โ๐ โ (๐๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐, ๐ฃโฉ ยท ๐ข)๐) โ (๐๐ป๐ข))) |
44 | | oveq2 7385 |
. . . . . 6
โข (๐ฃ = ๐ โ (๐๐ป๐ฃ) = (๐๐ป๐)) |
45 | | oveq1 7384 |
. . . . . . 7
โข (๐ฃ = ๐ โ (๐ฃ๐ป๐ข) = (๐๐ป๐ข)) |
46 | | opeq2 4851 |
. . . . . . . . . 10
โข (๐ฃ = ๐ โ โจ๐, ๐ฃโฉ = โจ๐, ๐โฉ) |
47 | 46 | oveq1d 7392 |
. . . . . . . . 9
โข (๐ฃ = ๐ โ (โจ๐, ๐ฃโฉ ยท ๐ข) = (โจ๐, ๐โฉ ยท ๐ข)) |
48 | 47 | oveqd 7394 |
. . . . . . . 8
โข (๐ฃ = ๐ โ (๐(โจ๐, ๐ฃโฉ ยท ๐ข)๐) = (๐(โจ๐, ๐โฉ ยท ๐ข)๐)) |
49 | 48 | eleq1d 2817 |
. . . . . . 7
โข (๐ฃ = ๐ โ ((๐(โจ๐, ๐ฃโฉ ยท ๐ข)๐) โ (๐๐ป๐ข) โ (๐(โจ๐, ๐โฉ ยท ๐ข)๐) โ (๐๐ป๐ข))) |
50 | 45, 49 | raleqbidv 3330 |
. . . . . 6
โข (๐ฃ = ๐ โ (โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐, ๐ฃโฉ ยท ๐ข)๐) โ (๐๐ป๐ข) โ โ๐ โ (๐๐ป๐ข)(๐(โจ๐, ๐โฉ ยท ๐ข)๐) โ (๐๐ป๐ข))) |
51 | 44, 50 | raleqbidv 3330 |
. . . . 5
โข (๐ฃ = ๐ โ (โ๐ โ (๐๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐, ๐ฃโฉ ยท ๐ข)๐) โ (๐๐ป๐ข) โ โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐ข)(๐(โจ๐, ๐โฉ ยท ๐ข)๐) โ (๐๐ป๐ข))) |
52 | | oveq2 7385 |
. . . . . . 7
โข (๐ข = ๐ โ (๐๐ป๐ข) = (๐๐ป๐)) |
53 | | oveq2 7385 |
. . . . . . . . 9
โข (๐ข = ๐ โ (โจ๐, ๐โฉ ยท ๐ข) = (โจ๐, ๐โฉ ยท ๐)) |
54 | 53 | oveqd 7394 |
. . . . . . . 8
โข (๐ข = ๐ โ (๐(โจ๐, ๐โฉ ยท ๐ข)๐) = (๐(โจ๐, ๐โฉ ยท ๐)๐)) |
55 | | oveq2 7385 |
. . . . . . . 8
โข (๐ข = ๐ โ (๐๐ป๐ข) = (๐๐ป๐)) |
56 | 54, 55 | eleq12d 2826 |
. . . . . . 7
โข (๐ข = ๐ โ ((๐(โจ๐, ๐โฉ ยท ๐ข)๐) โ (๐๐ป๐ข) โ (๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐))) |
57 | 52, 56 | raleqbidv 3330 |
. . . . . 6
โข (๐ข = ๐ โ (โ๐ โ (๐๐ป๐ข)(๐(โจ๐, ๐โฉ ยท ๐ข)๐) โ (๐๐ป๐ข) โ โ๐ โ (๐๐ป๐)(๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐))) |
58 | 57 | ralbidv 3176 |
. . . . 5
โข (๐ข = ๐ โ (โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐ข)(๐(โจ๐, ๐โฉ ยท ๐ข)๐) โ (๐๐ป๐ข) โ โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)(๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐))) |
59 | 43, 51, 58 | rspc3v 3608 |
. . . 4
โข ((๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (โ๐ค โ ๐ต โ๐ฃ โ ๐ต โ๐ข โ ๐ต โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข) โ โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)(๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐))) |
60 | 33, 34, 35, 59 | syl3anc 1371 |
. . 3
โข (๐ โ (โ๐ค โ ๐ต โ๐ฃ โ ๐ต โ๐ข โ ๐ต โ๐ โ (๐ค๐ป๐ฃ)โ๐ โ (๐ฃ๐ป๐ข)(๐(โจ๐ค, ๐ฃโฉ ยท ๐ข)๐) โ (๐ค๐ป๐ข) โ โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)(๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐))) |
61 | 32, 60 | mpd 15 |
. 2
โข (๐ โ โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)(๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐)) |
62 | | isthincd2lem2.4 |
. . 3
โข (๐ โ ๐น โ (๐๐ป๐)) |
63 | | isthincd2lem2.5 |
. . 3
โข (๐ โ ๐บ โ (๐๐ป๐)) |
64 | | oveq2 7385 |
. . . . 5
โข (๐ = ๐น โ (๐(โจ๐, ๐โฉ ยท ๐)๐) = (๐(โจ๐, ๐โฉ ยท ๐)๐น)) |
65 | 64 | eleq1d 2817 |
. . . 4
โข (๐ = ๐น โ ((๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐) โ (๐(โจ๐, ๐โฉ ยท ๐)๐น) โ (๐๐ป๐))) |
66 | | oveq1 7384 |
. . . . 5
โข (๐ = ๐บ โ (๐(โจ๐, ๐โฉ ยท ๐)๐น) = (๐บ(โจ๐, ๐โฉ ยท ๐)๐น)) |
67 | 66 | eleq1d 2817 |
. . . 4
โข (๐ = ๐บ โ ((๐(โจ๐, ๐โฉ ยท ๐)๐น) โ (๐๐ป๐) โ (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) โ (๐๐ป๐))) |
68 | 65, 67 | rspc2v 3604 |
. . 3
โข ((๐น โ (๐๐ป๐) โง ๐บ โ (๐๐ป๐)) โ (โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)(๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐) โ (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) โ (๐๐ป๐))) |
69 | 62, 63, 68 | syl2anc 584 |
. 2
โข (๐ โ (โ๐ โ (๐๐ป๐)โ๐ โ (๐๐ป๐)(๐(โจ๐, ๐โฉ ยท ๐)๐) โ (๐๐ป๐) โ (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) โ (๐๐ป๐))) |
70 | 61, 69 | mpd 15 |
1
โข (๐ โ (๐บ(โจ๐, ๐โฉ ยท ๐)๐น) โ (๐๐ป๐)) |