Step | Hyp | Ref
| Expression |
1 | | omeulem1 8533 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
โ๐ฅ โ On
โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) |
2 | | opex 5425 |
. . . . . . . . 9
โข
โจ๐ฅ, ๐ฆโฉ โ V |
3 | 2 | isseti 3462 |
. . . . . . . 8
โข
โ๐ง ๐ง = โจ๐ฅ, ๐ฆโฉ |
4 | | 19.41v 1954 |
. . . . . . . 8
โข
(โ๐ง(๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ (โ๐ง ๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
5 | 3, 4 | mpbiran 708 |
. . . . . . 7
โข
(โ๐ง(๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) |
6 | 5 | rexbii 3094 |
. . . . . 6
โข
(โ๐ฆ โ
๐ด โ๐ง(๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) |
7 | | rexcom4 3270 |
. . . . . 6
โข
(โ๐ฆ โ
๐ด โ๐ง(๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐งโ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
8 | 6, 7 | bitr3i 277 |
. . . . 5
โข
(โ๐ฆ โ
๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต โ โ๐งโ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
9 | 8 | rexbii 3094 |
. . . 4
โข
(โ๐ฅ โ On
โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต โ โ๐ฅ โ On โ๐งโ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
10 | | rexcom4 3270 |
. . . 4
โข
(โ๐ฅ โ On
โ๐งโ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
11 | 9, 10 | bitri 275 |
. . 3
โข
(โ๐ฅ โ On
โ๐ฆ โ ๐ด ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต โ โ๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
12 | 1, 11 | sylib 217 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
โ๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |
13 | | simp2rl 1243 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ง = โจ๐ฅ, ๐ฆโฉ) |
14 | | simp3rl 1247 |
. . . . . . . . . . . 12
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ก = โจ๐, ๐ โฉ) |
15 | | simp2rr 1244 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) |
16 | | simp3rr 1248 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ((๐ด ยทo ๐) +o ๐ ) = ๐ต) |
17 | 15, 16 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ )) |
18 | | simp11 1204 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ด โ On) |
19 | | simp13 1206 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ด โ โ
) |
20 | | simp2ll 1241 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ฅ โ On) |
21 | | simp2lr 1242 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ฆ โ ๐ด) |
22 | | simp3ll 1245 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ โ On) |
23 | | simp3lr 1246 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ โ ๐ด) |
24 | | omopth2 8535 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ โ On โง ๐ โ ๐ด)) โ (((๐ด ยทo ๐ฅ) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ ) โ (๐ฅ = ๐ โง ๐ฆ = ๐ ))) |
25 | 18, 19, 20, 21, 22, 23, 24 | syl222anc 1387 |
. . . . . . . . . . . . . 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 4836 |
. . . . . . . . . . . . 13
โข ((๐ฅ = ๐ โง ๐ฆ = ๐ ) โ โจ๐ฅ, ๐ฆโฉ = โจ๐, ๐ โฉ) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ โจ๐ฅ, ๐ฆโฉ = โจ๐, ๐ โฉ) |
29 | 14, 28 | eqtr4d 2776 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ก = โจ๐ฅ, ๐ฆโฉ) |
30 | 13, 29 | eqtr4d 2776 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โง ((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) โ ๐ง = ๐ก) |
31 | 30 | 3expia 1122 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง ((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต))) โ (((๐ โ On โง ๐ โ ๐ด) โง (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) โ ๐ง = ๐ก)) |
32 | 31 | exp4b 432 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ (((๐ฅ โ On โง ๐ฆ โ ๐ด) โง (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โ ((๐ โ On โง ๐ โ ๐ด) โ ((๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก)))) |
33 | 32 | expd 417 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ ((๐ฅ โ On โง ๐ฆ โ ๐ด) โ ((๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ ((๐ โ On โง ๐ โ ๐ด) โ ((๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก))))) |
34 | 33 | rexlimdvv 3201 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
(โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ ((๐ โ On โง ๐ โ ๐ด) โ ((๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก)))) |
35 | 34 | imp 408 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง
โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โ ((๐ โ On โง ๐ โ ๐ด) โ ((๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก))) |
36 | 35 | rexlimdvv 3201 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โง
โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) โ (โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ ๐ง = ๐ก)) |
37 | 36 | expimpd 455 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
((โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โง โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) โ ๐ง = ๐ก)) |
38 | 37 | alrimivv 1932 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
โ๐งโ๐ก((โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โง โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) โ ๐ง = ๐ก)) |
39 | | opeq1 4834 |
. . . . . . 7
โข (๐ฅ = ๐ โ โจ๐ฅ, ๐ฆโฉ = โจ๐, ๐ฆโฉ) |
40 | 39 | eqeq2d 2744 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ง = โจ๐ฅ, ๐ฆโฉ โ ๐ง = โจ๐, ๐ฆโฉ)) |
41 | | oveq2 7369 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐)) |
42 | 41 | oveq1d 7376 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ฆ)) |
43 | 42 | eqeq1d 2735 |
. . . . . 6
โข (๐ฅ = ๐ โ (((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต โ ((๐ด ยทo ๐) +o ๐ฆ) = ๐ต)) |
44 | 40, 43 | anbi12d 632 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ (๐ง = โจ๐, ๐ฆโฉ โง ((๐ด ยทo ๐) +o ๐ฆ) = ๐ต))) |
45 | | opeq2 4835 |
. . . . . . 7
โข (๐ฆ = ๐ โ โจ๐, ๐ฆโฉ = โจ๐, ๐ โฉ) |
46 | 45 | eqeq2d 2744 |
. . . . . 6
โข (๐ฆ = ๐ โ (๐ง = โจ๐, ๐ฆโฉ โ ๐ง = โจ๐, ๐ โฉ)) |
47 | | oveq2 7369 |
. . . . . . 7
โข (๐ฆ = ๐ โ ((๐ด ยทo ๐) +o ๐ฆ) = ((๐ด ยทo ๐) +o ๐ )) |
48 | 47 | eqeq1d 2735 |
. . . . . 6
โข (๐ฆ = ๐ โ (((๐ด ยทo ๐) +o ๐ฆ) = ๐ต โ ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) |
49 | 46, 48 | anbi12d 632 |
. . . . 5
โข (๐ฆ = ๐ โ ((๐ง = โจ๐, ๐ฆโฉ โง ((๐ด ยทo ๐) +o ๐ฆ) = ๐ต) โ (๐ง = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) |
50 | 44, 49 | cbvrex2vw 3227 |
. . . 4
โข
(โ๐ฅ โ On
โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐ โ On โ๐ โ ๐ด (๐ง = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) |
51 | | eqeq1 2737 |
. . . . . 6
โข (๐ง = ๐ก โ (๐ง = โจ๐, ๐ โฉ โ ๐ก = โจ๐, ๐ โฉ)) |
52 | 51 | anbi1d 631 |
. . . . 5
โข (๐ง = ๐ก โ ((๐ง = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) |
53 | 52 | 2rexbidv 3210 |
. . . 4
โข (๐ง = ๐ก โ (โ๐ โ On โ๐ โ ๐ด (๐ง = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต) โ โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) |
54 | 50, 53 | bitrid 283 |
. . 3
โข (๐ง = ๐ก โ (โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต))) |
55 | 54 | eu4 2612 |
. 2
โข
(โ!๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โ (โ๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โง โ๐งโ๐ก((โ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต) โง โ๐ โ On โ๐ โ ๐ด (๐ก = โจ๐, ๐ โฉ โง ((๐ด ยทo ๐) +o ๐ ) = ๐ต)) โ ๐ง = ๐ก))) |
56 | 12, 38, 55 | sylanbrc 584 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ด โ โ
) โ
โ!๐งโ๐ฅ โ On โ๐ฆ โ ๐ด (๐ง = โจ๐ฅ, ๐ฆโฉ โง ((๐ด ยทo ๐ฅ) +o ๐ฆ) = ๐ต)) |