Step | Hyp | Ref
| Expression |
1 | | trleile.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2733 |
. . . 4
β’
(leβπΎ) =
(leβπΎ) |
3 | 1, 2 | tleile 18315 |
. . 3
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π(leβπΎ)π β¨ π(leβπΎ)π)) |
4 | | 3simpc 1151 |
. . . . . 6
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π β π΅ β§ π β π΅)) |
5 | | brxp 5682 |
. . . . . 6
β’ (π(π΅ Γ π΅)π β (π β π΅ β§ π β π΅)) |
6 | 4, 5 | sylibr 233 |
. . . . 5
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β π(π΅ Γ π΅)π) |
7 | | brin 5158 |
. . . . . 6
β’ (π((leβπΎ) β© (π΅ Γ π΅))π β (π(leβπΎ)π β§ π(π΅ Γ π΅)π)) |
8 | 7 | rbaib 540 |
. . . . 5
β’ (π(π΅ Γ π΅)π β (π((leβπΎ) β© (π΅ Γ π΅))π β π(leβπΎ)π)) |
9 | 6, 8 | syl 17 |
. . . 4
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π((leβπΎ) β© (π΅ Γ π΅))π β π(leβπΎ)π)) |
10 | 4 | ancomd 463 |
. . . . . 6
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π β π΅ β§ π β π΅)) |
11 | | brxp 5682 |
. . . . . 6
β’ (π(π΅ Γ π΅)π β (π β π΅ β§ π β π΅)) |
12 | 10, 11 | sylibr 233 |
. . . . 5
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β π(π΅ Γ π΅)π) |
13 | | brin 5158 |
. . . . . 6
β’ (π((leβπΎ) β© (π΅ Γ π΅))π β (π(leβπΎ)π β§ π(π΅ Γ π΅)π)) |
14 | 13 | rbaib 540 |
. . . . 5
β’ (π(π΅ Γ π΅)π β (π((leβπΎ) β© (π΅ Γ π΅))π β π(leβπΎ)π)) |
15 | 12, 14 | syl 17 |
. . . 4
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π((leβπΎ) β© (π΅ Γ π΅))π β π(leβπΎ)π)) |
16 | 9, 15 | orbi12d 918 |
. . 3
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β ((π((leβπΎ) β© (π΅ Γ π΅))π β¨ π((leβπΎ) β© (π΅ Γ π΅))π) β (π(leβπΎ)π β¨ π(leβπΎ)π))) |
17 | 3, 16 | mpbird 257 |
. 2
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π((leβπΎ) β© (π΅ Γ π΅))π β¨ π((leβπΎ) β© (π΅ Γ π΅))π)) |
18 | | trleile.l |
. . . 4
β’ β€ =
((leβπΎ) β© (π΅ Γ π΅)) |
19 | 18 | breqi 5112 |
. . 3
β’ (π β€ π β π((leβπΎ) β© (π΅ Γ π΅))π) |
20 | 18 | breqi 5112 |
. . 3
β’ (π β€ π β π((leβπΎ) β© (π΅ Γ π΅))π) |
21 | 19, 20 | orbi12i 914 |
. 2
β’ ((π β€ π β¨ π β€ π) β (π((leβπΎ) β© (π΅ Γ π΅))π β¨ π((leβπΎ) β© (π΅ Γ π΅))π)) |
22 | 17, 21 | sylibr 233 |
1
β’ ((πΎ β Toset β§ π β π΅ β§ π β π΅) β (π β€ π β¨ π β€ π)) |