Step | Hyp | Ref
| Expression |
1 | | omeulem1 8581 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
โ๐ฅ โ On
โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) |
2 | | opex 5464 |
. . . . . . . . 9
โข
โจ๐ฅ, ๐ฆโฉ โ V |
3 | 2 | isseti 3489 |
. . . . . . . 8
โข
โ๐ง ๐ง = โจ๐ฅ, ๐ฆโฉ |
4 | | 19.41v 1953 |
. . . . . . . 8
โข
(โ๐ง(๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ (โ๐ง ๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
5 | 3, 4 | mpbiran 707 |
. . . . . . 7
โข
(โ๐ง(๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) |
6 | 5 | rexbii 3094 |
. . . . . 6
โข
(โ๐ฆ โ
๐ด โ๐ง(๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) |
7 | | rexcom4 3285 |
. . . . . 6
โข
(โ๐ฆ โ
๐ด โ๐ง(๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐งโ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
8 | 6, 7 | bitr3i 276 |
. . . . 5
โข
(โ๐ฆ โ
๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต โ โ๐งโ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
9 | 8 | rexbii 3094 |
. . . 4
โข
(โ๐ฅ โ On
โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต โ โ๐ฅ โ On โ๐งโ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
10 | | rexcom4 3285 |
. . . 4
โข
(โ๐ฅ โ On
โ๐งโ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
11 | 9, 10 | bitri 274 |
. . 3
โข
(โ๐ฅ โ On
โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต โ โ๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
12 | 1, 11 | sylib 217 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
โ๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
13 | | simp2rl 1242 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ง = โจ๐ฅ, ๐ฆโฉ) |
14 | | simp3rl 1246 |
. . . . . . . . . . . 12
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ก = โจ๐, ๐ โฉ) |
15 | | simp2rr 1243 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) |
16 | | simp3rr 1247 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ((๐ด ยทo ๐) +o ๐ ) = ๐ต) |
17 | 15, 16 | eqtr4d 2775 |
. . . . . . . . . . . . . 14
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ )) |
18 | | simp11 1203 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ด โ On) |
19 | | simp13 1205 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ด โ โ
) |
20 | | simp2ll 1240 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ฅ โ On) |
21 | | simp2lr 1241 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ฆ โ ๐ด) |
22 | | simp3ll 1244 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ โ On) |
23 | | simp3lr 1245 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ โ ๐ด) |
24 | | omopth2 8583 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ โ On โง ๐ โ ๐ด)) โ (((๐ด ยทo ๐ฅ) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ ) โ (๐ฅ = ๐ โง ๐ฆ = ๐ ))) |
25 | 18, 19, 20, 21, 22, 23, 24 | syl222anc 1386 |
. . . . . . . . . . . . . 14
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ (((๐ด ยทo ๐ฅ) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ ) โ (๐ฅ = ๐ โง ๐ฆ = ๐ ))) |
26 | 17, 25 | mpbid 231 |
. . . . . . . . . . . . 13
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ (๐ฅ = ๐ โง ๐ฆ = ๐ )) |
27 | | opeq12 4875 |
. . . . . . . . . . . . 13
โข ((๐ฅ = ๐ โง ๐ฆ = ๐ ) โ โจ๐ฅ, ๐ฆโฉ = โจ๐, ๐ โฉ) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ โจ๐ฅ, ๐ฆโฉ = โจ๐, ๐ โฉ) |
29 | 14, 28 | eqtr4d 2775 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ก = โจ๐ฅ, ๐ฆโฉ) |
30 | 13, 29 | eqtr4d 2775 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ง = ๐ก) |
31 | 30 | 3expia 1121 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต))) โ (((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) โ ๐ง = ๐ก)) |
32 | 31 | exp4b 431 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ (((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โ ((๐ โ On โง ๐ โ ๐ด) โ ((๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก)))) |
33 | 32 | expd 416 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ ((๐ฅ โ On โง ๐ฆ โ ๐ด) โ ((๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ ((๐ โ On โง ๐ โ ๐ด) โ ((๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก))))) |
34 | 33 | rexlimdvv 3210 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
(โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ ((๐ โ On โง ๐ โ ๐ด) โ ((๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก)))) |
35 | 34 | imp 407 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง
โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โ ((๐ โ On โง ๐ โ ๐ด) โ ((๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก))) |
36 | 35 | rexlimdvv 3210 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง
โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โ (โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก)) |
37 | 36 | expimpd 454 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
((โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โง โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) โ ๐ง = ๐ก)) |
38 | 37 | alrimivv 1931 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
โ๐งโ๐ก((โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โง โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) โ ๐ง = ๐ก)) |
39 | | opeq1 4873 |
. . . . . . 7
โข (๐ฅ = ๐ โ โจ๐ฅ, ๐ฆโฉ = โจ๐, ๐ฆโฉ) |
40 | 39 | eqeq2d 2743 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ง = โจ๐ฅ, ๐ฆโฉ โ ๐ง = โจ๐, ๐ฆโฉ)) |
41 | | oveq2 7416 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐)) |
42 | 41 | oveq1d 7423 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ฆ)) |
43 | 42 | eqeq1d 2734 |
. . . . . 6
โข (๐ฅ = ๐ โ (((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต โ ((๐ด ยทo ๐) +o ๐ฆ) = ๐ต)) |
44 | 40, 43 | anbi12d 631 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ (๐ง = โจ๐, ๐ฆโฉ โง ((๐ด ยทo ๐) +o ๐ฆ) = ๐ต))) |
45 | | opeq2 4874 |
. . . . . . 7
โข (๐ฆ = ๐ โ โจ๐, ๐ฆโฉ = โจ๐, ๐ โฉ) |
46 | 45 | eqeq2d 2743 |
. . . . . 6
โข (๐ฆ = ๐ โ (๐ง = โจ๐, ๐ฆโฉ โ ๐ง = โจ๐, ๐ โฉ)) |
47 | | oveq2 7416 |
. . . . . . 7
โข (๐ฆ = ๐ โ ((๐ด ยทo ๐) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ )) |
48 | 47 | eqeq1d 2734 |
. . . . . 6
โข (๐ฆ = ๐ โ (((๐ด ยทo ๐) +o ๐ฆ) = ๐ต โ ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) |
49 | 46, 48 | anbi12d 631 |
. . . . 5
โข (๐ฆ = ๐ โ ((๐ง = โจ๐, ๐ฆโฉ โง ((๐ด ยทo ๐) +o ๐ฆ) = ๐ต) โ (๐ง = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) |
50 | 44, 49 | cbvrex2vw 3239 |
. . . 4
โข
(โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐ โ On โ๐ โ ๐ด (๐ง = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) |
51 | | eqeq1 2736 |
. . . . . 6
โข (๐ง = ๐ก โ (๐ง = โจ๐, ๐ โฉ โ ๐ก = โจ๐, ๐ โฉ)) |
52 | 51 | anbi1d 630 |
. . . . 5
โข (๐ง = ๐ก โ ((๐ง = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) |
53 | 52 | 2rexbidv 3219 |
. . . 4
โข (๐ง = ๐ก โ (โ๐ โ On โ๐ โ ๐ด (๐ง = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) |
54 | 50, 53 | bitrid 282 |
. . 3
โข (๐ง = ๐ก โ (โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) |
55 | 54 | eu4 2611 |
. 2
โข
(โ!๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ (โ๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โง โ๐งโ๐ก((โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โง โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) โ ๐ง = ๐ก))) |
56 | 12, 38, 55 | sylanbrc 583 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
โ!๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |