Step | Hyp | Ref
| Expression |
1 | | vex 2740 |
. . . . . . . 8
โข ๐ โ V |
2 | | vex 2740 |
. . . . . . . 8
โข ๐ โ V |
3 | | eleq1 2240 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (๐ฅ โ (ฯ ร N)
โ ๐ โ (ฯ
ร N))) |
4 | 3 | anbi1d 465 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ((๐ฅ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โ (๐ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)))) |
5 | | eqeq1 2184 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ โ (๐ฅ = โจ๐ง, ๐คโฉ โ ๐ = โจ๐ง, ๐คโฉ)) |
6 | 5 | anbi1d 465 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ ((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โ (๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ))) |
7 | 6 | anbi1d 465 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ ((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
8 | 7 | 4exbidv 1870 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
9 | 4, 8 | anbi12d 473 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (((๐ฅ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))) โ ((๐ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))))) |
10 | | eleq1 2240 |
. . . . . . . . . 10
โข (๐ฆ = ๐ โ (๐ฆ โ (ฯ ร N)
โ ๐ โ (ฯ
ร N))) |
11 | 10 | anbi2d 464 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ ((๐ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โ (๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)))) |
12 | | eqeq1 2184 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ โ (๐ฆ = โจ๐ฃ, ๐ขโฉ โ ๐ = โจ๐ฃ, ๐ขโฉ)) |
13 | 12 | anbi2d 464 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ โ ((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โ (๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ))) |
14 | 13 | anbi1d 465 |
. . . . . . . . . 10
โข (๐ฆ = ๐ โ (((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ ((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
15 | 14 | 4exbidv 1870 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ (โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
16 | 11, 15 | anbi12d 473 |
. . . . . . . 8
โข (๐ฆ = ๐ โ (((๐ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))) โ ((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))))) |
17 | | df-enq0 7422 |
. . . . . . . 8
โข
~Q0 = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))} |
18 | 1, 2, 9, 16, 17 | brab 4272 |
. . . . . . 7
โข (๐ ~Q0
๐ โ ((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
19 | 18 | biimpi 120 |
. . . . . 6
โข (๐ ~Q0
๐ โ ((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
20 | | opeq12 3780 |
. . . . . . . . . . 11
โข ((๐ง = ๐ โง ๐ค = ๐) โ โจ๐ง, ๐คโฉ = โจ๐, ๐โฉ) |
21 | 20 | eqeq2d 2189 |
. . . . . . . . . 10
โข ((๐ง = ๐ โง ๐ค = ๐) โ (๐ = โจ๐ง, ๐คโฉ โ ๐ = โจ๐, ๐โฉ)) |
22 | 21 | anbi1d 465 |
. . . . . . . . 9
โข ((๐ง = ๐ โง ๐ค = ๐) โ ((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โ (๐ = โจ๐, ๐โฉ โง ๐ = โจ๐ฃ, ๐ขโฉ))) |
23 | | simpl 109 |
. . . . . . . . . . 11
โข ((๐ง = ๐ โง ๐ค = ๐) โ ๐ง = ๐) |
24 | 23 | oveq1d 5889 |
. . . . . . . . . 10
โข ((๐ง = ๐ โง ๐ค = ๐) โ (๐ง ยทo ๐ข) = (๐ ยทo ๐ข)) |
25 | | simpr 110 |
. . . . . . . . . . 11
โข ((๐ง = ๐ โง ๐ค = ๐) โ ๐ค = ๐) |
26 | 25 | oveq1d 5889 |
. . . . . . . . . 10
โข ((๐ง = ๐ โง ๐ค = ๐) โ (๐ค ยทo ๐ฃ) = (๐ ยทo ๐ฃ)) |
27 | 24, 26 | eqeq12d 2192 |
. . . . . . . . 9
โข ((๐ง = ๐ โง ๐ค = ๐) โ ((๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ) โ (๐ ยทo ๐ข) = (๐ ยทo ๐ฃ))) |
28 | 22, 27 | anbi12d 473 |
. . . . . . . 8
โข ((๐ง = ๐ โง ๐ค = ๐) โ (((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ ยทo ๐ข) = (๐ ยทo ๐ฃ)))) |
29 | | opeq12 3780 |
. . . . . . . . . . 11
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ โจ๐ฃ, ๐ขโฉ = โจ๐, ๐โฉ) |
30 | 29 | eqeq2d 2189 |
. . . . . . . . . 10
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (๐ = โจ๐ฃ, ๐ขโฉ โ ๐ = โจ๐, ๐โฉ)) |
31 | 30 | anbi2d 464 |
. . . . . . . . 9
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โ (๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ))) |
32 | | simpr 110 |
. . . . . . . . . . 11
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ ๐ข = ๐) |
33 | 32 | oveq2d 5890 |
. . . . . . . . . 10
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (๐ ยทo ๐ข) = (๐ ยทo ๐)) |
34 | | simpl 109 |
. . . . . . . . . . 11
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ ๐ฃ = ๐) |
35 | 34 | oveq2d 5890 |
. . . . . . . . . 10
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (๐ ยทo ๐ฃ) = (๐ ยทo ๐)) |
36 | 33, 35 | eqeq12d 2192 |
. . . . . . . . 9
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ ((๐ ยทo ๐ข) = (๐ ยทo ๐ฃ) โ (๐ ยทo ๐) = (๐ ยทo ๐))) |
37 | 31, 36 | anbi12d 473 |
. . . . . . . 8
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ ยทo ๐ข) = (๐ ยทo ๐ฃ)) โ ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
38 | 28, 37 | cbvex4v 1930 |
. . . . . . 7
โข
(โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ โ๐โ๐โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) |
39 | 38 | anbi2i 457 |
. . . . . 6
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))) โ ((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
40 | 19, 39 | sylib 122 |
. . . . 5
โข (๐ ~Q0
๐ โ ((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง โ๐โ๐โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
41 | | 19.42vv 1911 |
. . . . 5
โข
(โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
42 | 40, 41 | sylibr 134 |
. . . 4
โข (๐ ~Q0
๐ โ โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
43 | | 19.42vv 1911 |
. . . . 5
โข
(โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
44 | 43 | 2exbii 1606 |
. . . 4
โข
(โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
45 | 42, 44 | sylibr 134 |
. . 3
โข (๐ ~Q0
๐ โ โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
46 | | pm3.22 265 |
. . . . . . 7
โข ((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โ (๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N))) |
47 | 46 | adantr 276 |
. . . . . 6
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ (๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N))) |
48 | | pm3.22 265 |
. . . . . . 7
โข ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โ (๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ)) |
49 | 48 | ad2antrl 490 |
. . . . . 6
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ (๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ)) |
50 | | simprr 531 |
. . . . . . . 8
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ (๐ ยทo ๐) = (๐ ยทo ๐)) |
51 | | eleq1 2240 |
. . . . . . . . . . . . . 14
โข (๐ = โจ๐, ๐โฉ โ (๐ โ (ฯ ร N)
โ โจ๐, ๐โฉ โ (ฯ ร
N))) |
52 | | opelxp 4656 |
. . . . . . . . . . . . . 14
โข
(โจ๐, ๐โฉ โ (ฯ ร
N) โ (๐
โ ฯ โง ๐
โ N)) |
53 | 51, 52 | bitrdi 196 |
. . . . . . . . . . . . 13
โข (๐ = โจ๐, ๐โฉ โ (๐ โ (ฯ ร N)
โ (๐ โ ฯ
โง ๐ โ
N))) |
54 | 53 | biimpcd 159 |
. . . . . . . . . . . 12
โข (๐ โ (ฯ ร
N) โ (๐
= โจ๐, ๐โฉ โ (๐ โ ฯ โง ๐ โ
N))) |
55 | | eleq1 2240 |
. . . . . . . . . . . . . 14
โข (๐ = โจ๐, ๐โฉ โ (๐ โ (ฯ ร N)
โ โจ๐, ๐โฉ โ (ฯ ร
N))) |
56 | | opelxp 4656 |
. . . . . . . . . . . . . 14
โข
(โจ๐, ๐โฉ โ (ฯ ร
N) โ (๐
โ ฯ โง ๐
โ N)) |
57 | 55, 56 | bitrdi 196 |
. . . . . . . . . . . . 13
โข (๐ = โจ๐, ๐โฉ โ (๐ โ (ฯ ร N)
โ (๐ โ ฯ
โง ๐ โ
N))) |
58 | 57 | biimpcd 159 |
. . . . . . . . . . . 12
โข (๐ โ (ฯ ร
N) โ (๐
= โจ๐, ๐โฉ โ (๐ โ ฯ โง ๐ โ
N))) |
59 | 54, 58 | im2anan9 598 |
. . . . . . . . . . 11
โข ((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โ ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โ ((๐ โ ฯ โง ๐ โ N) โง (๐ โ ฯ โง ๐ โ
N)))) |
60 | 59 | imp 124 |
. . . . . . . . . 10
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง (๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ)) โ ((๐ โ ฯ โง ๐ โ N) โง (๐ โ ฯ โง ๐ โ
N))) |
61 | 60 | adantrr 479 |
. . . . . . . . 9
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ((๐ โ ฯ โง ๐ โ N) โง (๐ โ ฯ โง ๐ โ
N))) |
62 | | pinn 7307 |
. . . . . . . . . . . 12
โข (๐ โ N โ
๐ โ
ฯ) |
63 | | nnmcom 6489 |
. . . . . . . . . . . 12
โข ((๐ โ ฯ โง ๐ โ ฯ) โ (๐ ยทo ๐) = (๐ ยทo ๐)) |
64 | 62, 63 | sylan2 286 |
. . . . . . . . . . 11
โข ((๐ โ ฯ โง ๐ โ N) โ
(๐ ยทo
๐) = (๐ ยทo ๐)) |
65 | | pinn 7307 |
. . . . . . . . . . . 12
โข (๐ โ N โ
๐ โ
ฯ) |
66 | | nnmcom 6489 |
. . . . . . . . . . . 12
โข ((๐ โ ฯ โง ๐ โ ฯ) โ (๐ ยทo ๐) = (๐ ยทo ๐)) |
67 | 65, 66 | sylan 283 |
. . . . . . . . . . 11
โข ((๐ โ N โง
๐ โ ฯ) โ
(๐ ยทo
๐) = (๐ ยทo ๐)) |
68 | 64, 67 | eqeqan12d 2193 |
. . . . . . . . . 10
โข (((๐ โ ฯ โง ๐ โ N) โง
(๐ โ N
โง ๐ โ ฯ))
โ ((๐
ยทo ๐) =
(๐ ยทo
๐) โ (๐ ยทo ๐) = (๐ ยทo ๐))) |
69 | 68 | an42s 589 |
. . . . . . . . 9
โข (((๐ โ ฯ โง ๐ โ N) โง
(๐ โ ฯ โง
๐ โ N))
โ ((๐
ยทo ๐) =
(๐ ยทo
๐) โ (๐ ยทo ๐) = (๐ ยทo ๐))) |
70 | 61, 69 | syl 14 |
. . . . . . . 8
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ((๐ ยทo ๐) = (๐ ยทo ๐) โ (๐ ยทo ๐) = (๐ ยทo ๐))) |
71 | 50, 70 | mpbid 147 |
. . . . . . 7
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ (๐ ยทo ๐) = (๐ ยทo ๐)) |
72 | 71 | eqcomd 2183 |
. . . . . 6
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ (๐ ยทo ๐) = (๐ ยทo ๐)) |
73 | 47, 49, 72 | jca32 310 |
. . . . 5
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
74 | 73 | 2eximi 1601 |
. . . 4
โข
(โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
75 | 74 | 2eximi 1601 |
. . 3
โข
(โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
76 | 45, 75 | syl 14 |
. 2
โข (๐ ~Q0
๐ โ โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
77 | | exrot4 1691 |
. . 3
โข
(โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
78 | | 19.42vv 1911 |
. . . . 5
โข
(โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
79 | 78 | 2exbii 1606 |
. . . 4
โข
(โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
80 | | 19.42vv 1911 |
. . . . 5
โข
(โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
81 | | opeq12 3780 |
. . . . . . . . . 10
โข ((๐ง = ๐ โง ๐ค = ๐) โ โจ๐ง, ๐คโฉ = โจ๐, ๐โฉ) |
82 | 81 | eqeq2d 2189 |
. . . . . . . . 9
โข ((๐ง = ๐ โง ๐ค = ๐) โ (๐ = โจ๐ง, ๐คโฉ โ ๐ = โจ๐, ๐โฉ)) |
83 | 82 | anbi1d 465 |
. . . . . . . 8
โข ((๐ง = ๐ โง ๐ค = ๐) โ ((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โ (๐ = โจ๐, ๐โฉ โง ๐ = โจ๐ฃ, ๐ขโฉ))) |
84 | | simpl 109 |
. . . . . . . . . 10
โข ((๐ง = ๐ โง ๐ค = ๐) โ ๐ง = ๐) |
85 | 84 | oveq1d 5889 |
. . . . . . . . 9
โข ((๐ง = ๐ โง ๐ค = ๐) โ (๐ง ยทo ๐ข) = (๐ ยทo ๐ข)) |
86 | | simpr 110 |
. . . . . . . . . 10
โข ((๐ง = ๐ โง ๐ค = ๐) โ ๐ค = ๐) |
87 | 86 | oveq1d 5889 |
. . . . . . . . 9
โข ((๐ง = ๐ โง ๐ค = ๐) โ (๐ค ยทo ๐ฃ) = (๐ ยทo ๐ฃ)) |
88 | 85, 87 | eqeq12d 2192 |
. . . . . . . 8
โข ((๐ง = ๐ โง ๐ค = ๐) โ ((๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ) โ (๐ ยทo ๐ข) = (๐ ยทo ๐ฃ))) |
89 | 83, 88 | anbi12d 473 |
. . . . . . 7
โข ((๐ง = ๐ โง ๐ค = ๐) โ (((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ ยทo ๐ข) = (๐ ยทo ๐ฃ)))) |
90 | | opeq12 3780 |
. . . . . . . . . 10
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ โจ๐ฃ, ๐ขโฉ = โจ๐, ๐โฉ) |
91 | 90 | eqeq2d 2189 |
. . . . . . . . 9
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (๐ = โจ๐ฃ, ๐ขโฉ โ ๐ = โจ๐, ๐โฉ)) |
92 | 91 | anbi2d 464 |
. . . . . . . 8
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โ (๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ))) |
93 | | simpr 110 |
. . . . . . . . . 10
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ ๐ข = ๐) |
94 | 93 | oveq2d 5890 |
. . . . . . . . 9
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (๐ ยทo ๐ข) = (๐ ยทo ๐)) |
95 | | simpl 109 |
. . . . . . . . . 10
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ ๐ฃ = ๐) |
96 | 95 | oveq2d 5890 |
. . . . . . . . 9
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (๐ ยทo ๐ฃ) = (๐ ยทo ๐)) |
97 | 94, 96 | eqeq12d 2192 |
. . . . . . . 8
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ ((๐ ยทo ๐ข) = (๐ ยทo ๐ฃ) โ (๐ ยทo ๐) = (๐ ยทo ๐))) |
98 | 92, 97 | anbi12d 473 |
. . . . . . 7
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ ยทo ๐ข) = (๐ ยทo ๐ฃ)) โ ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐)))) |
99 | 89, 98 | cbvex4v 1930 |
. . . . . 6
โข
(โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ โ๐โ๐โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) |
100 | | eleq1 2240 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (๐ฅ โ (ฯ ร N)
โ ๐ โ (ฯ
ร N))) |
101 | 100 | anbi1d 465 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ((๐ฅ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โ (๐ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)))) |
102 | | eqeq1 2184 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ โ (๐ฅ = โจ๐ง, ๐คโฉ โ ๐ = โจ๐ง, ๐คโฉ)) |
103 | 102 | anbi1d 465 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ ((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โ (๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ))) |
104 | 103 | anbi1d 465 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ ((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
105 | 104 | 4exbidv 1870 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
106 | 101, 105 | anbi12d 473 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (((๐ฅ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))) โ ((๐ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))))) |
107 | | eleq1 2240 |
. . . . . . . . . 10
โข (๐ฆ = ๐ โ (๐ฆ โ (ฯ ร N)
โ ๐ โ (ฯ
ร N))) |
108 | 107 | anbi2d 464 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ ((๐ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โ (๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)))) |
109 | | eqeq1 2184 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ โ (๐ฆ = โจ๐ฃ, ๐ขโฉ โ ๐ = โจ๐ฃ, ๐ขโฉ)) |
110 | 109 | anbi2d 464 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ โ ((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โ (๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ))) |
111 | 110 | anbi1d 465 |
. . . . . . . . . 10
โข (๐ฆ = ๐ โ (((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ ((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
112 | 111 | 4exbidv 1870 |
. . . . . . . . 9
โข (๐ฆ = ๐ โ (โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)) โ โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
113 | 108, 112 | anbi12d 473 |
. . . . . . . 8
โข (๐ฆ = ๐ โ (((๐ โ (ฯ ร N)
โง ๐ฆ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))) โ ((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))))) |
114 | 2, 1, 106, 113, 17 | brab 4272 |
. . . . . . 7
โข (๐ ~Q0
๐ โ ((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ)))) |
115 | 114 | biimpri 133 |
. . . . . 6
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ = โจ๐ง, ๐คโฉ โง ๐ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทo ๐ข) = (๐ค ยทo ๐ฃ))) โ ๐ ~Q0 ๐) |
116 | 99, 115 | sylan2br 288 |
. . . . 5
โข (((๐ โ (ฯ ร
N) โง ๐
โ (ฯ ร N)) โง โ๐โ๐โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ๐ ~Q0 ๐) |
117 | 80, 116 | sylbi 121 |
. . . 4
โข
(โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง โ๐โ๐((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ๐ ~Q0 ๐) |
118 | 79, 117 | sylbi 121 |
. . 3
โข
(โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ๐ ~Q0 ๐) |
119 | 77, 118 | sylbi 121 |
. 2
โข
(โ๐โ๐โ๐โ๐((๐ โ (ฯ ร N)
โง ๐ โ (ฯ
ร N)) โง ((๐ = โจ๐, ๐โฉ โง ๐ = โจ๐, ๐โฉ) โง (๐ ยทo ๐) = (๐ ยทo ๐))) โ ๐ ~Q0 ๐) |
120 | 76, 119 | syl 14 |
1
โข (๐ ~Q0
๐ โ ๐ ~Q0 ๐) |