Step | Hyp | Ref
| Expression |
1 | | posrasymb.l |
. . . . 5
β’ β€ =
((leβπΎ) β© (π΅ Γ π΅)) |
2 | 1 | breqi 5154 |
. . . 4
β’ (π β€ π β π((leβπΎ) β© (π΅ Γ π΅))π) |
3 | | simp2 1137 |
. . . . . 6
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β π β π΅) |
4 | | simp3 1138 |
. . . . . 6
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β π β π΅) |
5 | | brxp 5725 |
. . . . . 6
β’ (π(π΅ Γ π΅)π β (π β π΅ β§ π β π΅)) |
6 | 3, 4, 5 | sylanbrc 583 |
. . . . 5
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β π(π΅ Γ π΅)π) |
7 | | brin 5200 |
. . . . . 6
β’ (π((leβπΎ) β© (π΅ Γ π΅))π β (π(leβπΎ)π β§ π(π΅ Γ π΅)π)) |
8 | 7 | rbaib 539 |
. . . . 5
β’ (π(π΅ Γ π΅)π β (π((leβπΎ) β© (π΅ Γ π΅))π β π(leβπΎ)π)) |
9 | 6, 8 | syl 17 |
. . . 4
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π((leβπΎ) β© (π΅ Γ π΅))π β π(leβπΎ)π)) |
10 | 2, 9 | bitrid 282 |
. . 3
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β€ π β π(leβπΎ)π)) |
11 | 1 | breqi 5154 |
. . . 4
β’ (π β€ π β π((leβπΎ) β© (π΅ Γ π΅))π) |
12 | | brxp 5725 |
. . . . . 6
β’ (π(π΅ Γ π΅)π β (π β π΅ β§ π β π΅)) |
13 | 4, 3, 12 | sylanbrc 583 |
. . . . 5
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β π(π΅ Γ π΅)π) |
14 | | brin 5200 |
. . . . . 6
β’ (π((leβπΎ) β© (π΅ Γ π΅))π β (π(leβπΎ)π β§ π(π΅ Γ π΅)π)) |
15 | 14 | rbaib 539 |
. . . . 5
β’ (π(π΅ Γ π΅)π β (π((leβπΎ) β© (π΅ Γ π΅))π β π(leβπΎ)π)) |
16 | 13, 15 | syl 17 |
. . . 4
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π((leβπΎ) β© (π΅ Γ π΅))π β π(leβπΎ)π)) |
17 | 11, 16 | bitrid 282 |
. . 3
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β€ π β π(leβπΎ)π)) |
18 | 10, 17 | anbi12d 631 |
. 2
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β ((π β€ π β§ π β€ π) β (π(leβπΎ)π β§ π(leβπΎ)π))) |
19 | | posrasymb.b |
. . 3
β’ π΅ = (BaseβπΎ) |
20 | | eqid 2732 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
21 | 19, 20 | posasymb 18271 |
. 2
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β ((π(leβπΎ)π β§ π(leβπΎ)π) β π = π)) |
22 | 18, 21 | bitrd 278 |
1
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β ((π β€ π β§ π β€ π) β π = π)) |