Step | Hyp | Ref
| Expression |
1 | | trgcgrg.p |
. . 3
β’ π = (BaseβπΊ) |
2 | | trgcgrg.m |
. . 3
β’ β =
(distβπΊ) |
3 | | trgcgrg.r |
. . 3
β’ βΌ =
(cgrGβπΊ) |
4 | | trgcgrg.g |
. . 3
β’ (π β πΊ β TarskiG) |
5 | | iscgrglt.d |
. . 3
β’ (π β π· β β) |
6 | | iscgrglt.a |
. . 3
β’ (π β π΄:π·βΆπ) |
7 | | iscgrglt.b |
. . 3
β’ (π β π΅:π·βΆπ) |
8 | 1, 2, 3, 4, 5, 6, 7 | iscgrgd 27504 |
. 2
β’ (π β (π΄ βΌ π΅ β βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
9 | | simp2 1138 |
. . . . 5
β’ (((π β§ (π β dom π΄ β§ π β dom π΄)) β§ ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β§ π < π) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
10 | 9 | 3exp 1120 |
. . . 4
β’ ((π β§ (π β dom π΄ β§ π β dom π΄)) β (((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β (π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
11 | 10 | ralimdvva 3198 |
. . 3
β’ (π β (βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
12 | | breq1 5112 |
. . . . . 6
β’ (π = π β (π < π β π < π)) |
13 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (π΄βπ) = (π΄βπ)) |
14 | 13 | oveq1d 7376 |
. . . . . . 7
β’ (π = π β ((π΄βπ) β (π΄βπ)) = ((π΄βπ) β (π΄βπ))) |
15 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (π΅βπ) = (π΅βπ)) |
16 | 15 | oveq1d 7376 |
. . . . . . 7
β’ (π = π β ((π΅βπ) β (π΅βπ)) = ((π΅βπ) β (π΅βπ))) |
17 | 14, 16 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β (((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
18 | 12, 17 | imbi12d 345 |
. . . . 5
β’ (π = π β ((π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) β (π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
19 | | breq2 5113 |
. . . . . 6
β’ (π = π β (π < π β π < π)) |
20 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (π΄βπ) = (π΄βπ)) |
21 | 20 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β ((π΄βπ) β (π΄βπ)) = ((π΄βπ) β (π΄βπ))) |
22 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (π΅βπ) = (π΅βπ)) |
23 | 22 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β ((π΅βπ) β (π΅βπ)) = ((π΅βπ) β (π΅βπ))) |
24 | 21, 23 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β (((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
25 | 19, 24 | imbi12d 345 |
. . . . 5
β’ (π = π β ((π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) β (π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
26 | 18, 25 | cbvral2vw 3226 |
. . . 4
β’
(βπ β
dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) β βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
27 | | simpllr 775 |
. . . . . . . . . 10
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β π β dom π΄) |
28 | | simplr 768 |
. . . . . . . . . 10
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β π β dom π΄) |
29 | | simp-4r 783 |
. . . . . . . . . 10
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
30 | 27, 28, 29 | jca31 516 |
. . . . . . . . 9
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β ((π β dom π΄ β§ π β dom π΄) β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
31 | | simpr 486 |
. . . . . . . . 9
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β π < π) |
32 | 18, 25 | rspc2va 3593 |
. . . . . . . . 9
β’ (((π β dom π΄ β§ π β dom π΄) β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β (π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
33 | 30, 31, 32 | sylc 65 |
. . . . . . . 8
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
34 | | eqid 2733 |
. . . . . . . . . . 11
β’
(ItvβπΊ) =
(ItvβπΊ) |
35 | 4 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β πΊ β TarskiG) |
36 | 6 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β π΄:π·βΆπ) |
37 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β π β dom π΄) |
38 | 36 | fdmd 6683 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β dom π΄ = π·) |
39 | 37, 38 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β π β π·) |
40 | 36, 39 | ffvelcdmd 7040 |
. . . . . . . . . . . 12
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β (π΄βπ) β π) |
41 | 40 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β (π΄βπ) β π) |
42 | 7 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β π΅:π·βΆπ) |
43 | 42, 39 | ffvelcdmd 7040 |
. . . . . . . . . . . 12
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β (π΅βπ) β π) |
44 | 43 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β (π΅βπ) β π) |
45 | 1, 2, 34, 35, 41, 44 | tgcgrtriv 27475 |
. . . . . . . . . 10
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
46 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β π = π) |
47 | 46 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β (π΄βπ) = (π΄βπ)) |
48 | 47 | oveq2d 7377 |
. . . . . . . . . 10
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β ((π΄βπ) β (π΄βπ)) = ((π΄βπ) β (π΄βπ))) |
49 | 46 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β (π΅βπ) = (π΅βπ)) |
50 | 49 | oveq2d 7377 |
. . . . . . . . . 10
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β ((π΅βπ) β (π΅βπ)) = ((π΅βπ) β (π΅βπ))) |
51 | 45, 48, 50 | 3eqtr3d 2781 |
. . . . . . . . 9
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
52 | 51 | adantl3r 749 |
. . . . . . . 8
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π = π) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
53 | 4 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β πΊ β TarskiG) |
54 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β π β dom π΄) |
55 | 54, 38 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β π β π·) |
56 | 36, 55 | ffvelcdmd 7040 |
. . . . . . . . . . 11
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β (π΄βπ) β π) |
57 | 56 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β (π΄βπ) β π) |
58 | 57 | adantl3r 749 |
. . . . . . . . 9
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β (π΄βπ) β π) |
59 | 40 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β (π΄βπ) β π) |
60 | 59 | adantl3r 749 |
. . . . . . . . 9
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β (π΄βπ) β π) |
61 | 42, 55 | ffvelcdmd 7040 |
. . . . . . . . . . 11
β’ (((π β§ π β dom π΄) β§ π β dom π΄) β (π΅βπ) β π) |
62 | 61 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β (π΅βπ) β π) |
63 | 62 | adantl3r 749 |
. . . . . . . . 9
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β (π΅βπ) β π) |
64 | 43 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β (π΅βπ) β π) |
65 | 64 | adantl3r 749 |
. . . . . . . . 9
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β (π΅βπ) β π) |
66 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β π β dom π΄) |
67 | | simpllr 775 |
. . . . . . . . . . 11
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β π β dom π΄) |
68 | | simp-4r 783 |
. . . . . . . . . . 11
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
69 | 66, 67, 68 | jca31 516 |
. . . . . . . . . 10
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β ((π β dom π΄ β§ π β dom π΄) β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
70 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β π < π) |
71 | | breq1 5112 |
. . . . . . . . . . . 12
β’ (π = π β (π < π β π < π)) |
72 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ) = (π΄βπ)) |
73 | 72 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (π = π β ((π΄βπ) β (π΄βπ)) = ((π΄βπ) β (π΄βπ))) |
74 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΅βπ) = (π΅βπ)) |
75 | 74 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (π = π β ((π΅βπ) β (π΅βπ)) = ((π΅βπ) β (π΅βπ))) |
76 | 73, 75 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π = π β (((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
77 | 71, 76 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β ((π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) β (π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
78 | | breq2 5113 |
. . . . . . . . . . . 12
β’ (π = π β (π < π β π < π)) |
79 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ) = (π΄βπ)) |
80 | 79 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ (π = π β ((π΄βπ) β (π΄βπ)) = ((π΄βπ) β (π΄βπ))) |
81 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΅βπ) = (π΅βπ)) |
82 | 81 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ (π = π β ((π΅βπ) β (π΅βπ)) = ((π΅βπ) β (π΅βπ))) |
83 | 80, 82 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π = π β (((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
84 | 78, 83 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β ((π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) β (π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
85 | 77, 84 | rspc2va 3593 |
. . . . . . . . . 10
β’ (((π β dom π΄ β§ π β dom π΄) β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β (π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
86 | 69, 70, 85 | sylc 65 |
. . . . . . . . 9
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
87 | 1, 2, 34, 53, 58, 60, 63, 65, 86 | tgcgrcomlr 27471 |
. . . . . . . 8
β’
(((((π β§
βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β§ π < π) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
88 | 6 | fdmd 6683 |
. . . . . . . . . . . 12
β’ (π β dom π΄ = π·) |
89 | 88, 5 | eqsstrd 3986 |
. . . . . . . . . . 11
β’ (π β dom π΄ β β) |
90 | 89 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β dom π΄ β β) |
91 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β π β dom π΄) |
92 | 90, 91 | sseldd 3949 |
. . . . . . . . 9
β’ ((((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β π β β) |
93 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β π β dom π΄) |
94 | 90, 93 | sseldd 3949 |
. . . . . . . . 9
β’ ((((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β π β β) |
95 | 92, 94 | lttri4d 11304 |
. . . . . . . 8
β’ ((((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β (π < π β¨ π = π β¨ π < π)) |
96 | 33, 52, 87, 95 | mpjao3dan 1432 |
. . . . . . 7
β’ ((((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ π β dom π΄) β§ π β dom π΄) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
97 | 96 | anasss 468 |
. . . . . 6
β’ (((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β§ (π β dom π΄ β§ π β dom π΄)) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
98 | 97 | ralrimivva 3194 |
. . . . 5
β’ ((π β§ βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) β βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) |
99 | 98 | ex 414 |
. . . 4
β’ (π β (βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) β βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
100 | 26, 99 | biimtrrid 242 |
. . 3
β’ (π β (βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))) β βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
101 | 11, 100 | impbid 211 |
. 2
β’ (π β (βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)) β βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
102 | 8, 101 | bitrd 279 |
1
β’ (π β (π΄ βΌ π΅ β βπ β dom π΄βπ β dom π΄(π < π β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |