Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ps-1 Structured version   Visualization version   GIF version

Theorem ps-1 33605
Description: The join of two atoms 𝑅 𝑆 (specifying a projective geometry line) is determined uniquely by any two atoms (specifying two points) less than or equal to that join. Part of Lemma 16.4 of [MaedaMaeda] p. 69, showing projective space postulate PS1 in [MaedaMaeda] p. 67. (Contributed by NM, 15-Nov-2011.)
Hypotheses
Ref Expression
ps1.l = (le‘𝐾)
ps1.j = (join‘𝐾)
ps1.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
ps-1 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) (𝑅 𝑆) ↔ (𝑃 𝑄) = (𝑅 𝑆)))

Proof of Theorem ps-1
StepHypRef Expression
1 oveq1 6534 . . . . . 6 (𝑅 = 𝑃 → (𝑅 𝑆) = (𝑃 𝑆))
21breq2d 4589 . . . . 5 (𝑅 = 𝑃 → ((𝑃 𝑄) (𝑅 𝑆) ↔ (𝑃 𝑄) (𝑃 𝑆)))
31eqeq2d 2619 . . . . 5 (𝑅 = 𝑃 → ((𝑃 𝑄) = (𝑅 𝑆) ↔ (𝑃 𝑄) = (𝑃 𝑆)))
42, 3imbi12d 332 . . . 4 (𝑅 = 𝑃 → (((𝑃 𝑄) (𝑅 𝑆) → (𝑃 𝑄) = (𝑅 𝑆)) ↔ ((𝑃 𝑄) (𝑃 𝑆) → (𝑃 𝑄) = (𝑃 𝑆))))
54eqcoms 2617 . . 3 (𝑃 = 𝑅 → (((𝑃 𝑄) (𝑅 𝑆) → (𝑃 𝑄) = (𝑅 𝑆)) ↔ ((𝑃 𝑄) (𝑃 𝑆) → (𝑃 𝑄) = (𝑃 𝑆))))
6 simp3 1055 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅 ∧ (𝑃 𝑄) (𝑅 𝑆)) → (𝑃 𝑄) (𝑅 𝑆))
7 simp1 1053 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝐾 ∈ HL)
8 simp21 1086 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝑃𝐴)
9 simp3l 1081 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝑅𝐴)
10 ps1.j . . . . . . . . . . . . 13 = (join‘𝐾)
11 ps1.a . . . . . . . . . . . . 13 𝐴 = (Atoms‘𝐾)
1210, 11hlatjcom 33496 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴) → (𝑃 𝑅) = (𝑅 𝑃))
137, 8, 9, 12syl3anc 1317 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → (𝑃 𝑅) = (𝑅 𝑃))
14133ad2ant1 1074 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅 ∧ (𝑃 𝑄) (𝑅 𝑆)) → (𝑃 𝑅) = (𝑅 𝑃))
15 hllat 33492 . . . . . . . . . . . . . . . 16 (𝐾 ∈ HL → 𝐾 ∈ Lat)
16153ad2ant1 1074 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝐾 ∈ Lat)
17 eqid 2609 . . . . . . . . . . . . . . . . 17 (Base‘𝐾) = (Base‘𝐾)
1817, 11atbase 33418 . . . . . . . . . . . . . . . 16 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
198, 18syl 17 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝑃 ∈ (Base‘𝐾))
20 simp22 1087 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝑄𝐴)
2117, 11atbase 33418 . . . . . . . . . . . . . . . 16 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
2220, 21syl 17 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝑄 ∈ (Base‘𝐾))
23 simp3r 1082 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝑆𝐴)
2417, 10, 11hlatjcl 33495 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) → (𝑅 𝑆) ∈ (Base‘𝐾))
257, 9, 23, 24syl3anc 1317 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → (𝑅 𝑆) ∈ (Base‘𝐾))
26 ps1.l . . . . . . . . . . . . . . . 16 = (le‘𝐾)
2717, 26, 10latjle12 16834 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑅 𝑆) ∈ (Base‘𝐾))) → ((𝑃 (𝑅 𝑆) ∧ 𝑄 (𝑅 𝑆)) ↔ (𝑃 𝑄) (𝑅 𝑆)))
2816, 19, 22, 25, 27syl13anc 1319 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 (𝑅 𝑆) ∧ 𝑄 (𝑅 𝑆)) ↔ (𝑃 𝑄) (𝑅 𝑆)))
29 simpl 471 . . . . . . . . . . . . . 14 ((𝑃 (𝑅 𝑆) ∧ 𝑄 (𝑅 𝑆)) → 𝑃 (𝑅 𝑆))
3028, 29syl6bir 242 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) (𝑅 𝑆) → 𝑃 (𝑅 𝑆)))
3130adantr 479 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → ((𝑃 𝑄) (𝑅 𝑆) → 𝑃 (𝑅 𝑆)))
32 simpl1 1056 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → 𝐾 ∈ HL)
33 simpl21 1131 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → 𝑃𝐴)
34 simpl3r 1109 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → 𝑆𝐴)
35 simpl3l 1108 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → 𝑅𝐴)
36 simpr 475 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → 𝑃𝑅)
3726, 10, 11hlatexchb1 33521 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑆𝐴𝑅𝐴) ∧ 𝑃𝑅) → (𝑃 (𝑅 𝑆) ↔ (𝑅 𝑃) = (𝑅 𝑆)))
3832, 33, 34, 35, 36, 37syl131anc 1330 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → (𝑃 (𝑅 𝑆) ↔ (𝑅 𝑃) = (𝑅 𝑆)))
3931, 38sylibd 227 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → ((𝑃 𝑄) (𝑅 𝑆) → (𝑅 𝑃) = (𝑅 𝑆)))
40393impia 1252 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅 ∧ (𝑃 𝑄) (𝑅 𝑆)) → (𝑅 𝑃) = (𝑅 𝑆))
4114, 40eqtrd 2643 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅 ∧ (𝑃 𝑄) (𝑅 𝑆)) → (𝑃 𝑅) = (𝑅 𝑆))
426, 41breqtrrd 4605 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅 ∧ (𝑃 𝑄) (𝑅 𝑆)) → (𝑃 𝑄) (𝑃 𝑅))
43423expia 1258 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → ((𝑃 𝑄) (𝑅 𝑆) → (𝑃 𝑄) (𝑃 𝑅)))
4417, 10, 11hlatjcl 33495 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴) → (𝑃 𝑅) ∈ (Base‘𝐾))
457, 8, 9, 44syl3anc 1317 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → (𝑃 𝑅) ∈ (Base‘𝐾))
4617, 26, 10latjle12 16834 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑅) ∈ (Base‘𝐾))) → ((𝑃 (𝑃 𝑅) ∧ 𝑄 (𝑃 𝑅)) ↔ (𝑃 𝑄) (𝑃 𝑅)))
4716, 19, 22, 45, 46syl13anc 1319 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 (𝑃 𝑅) ∧ 𝑄 (𝑃 𝑅)) ↔ (𝑃 𝑄) (𝑃 𝑅)))
48 simpr 475 . . . . . . . . . 10 ((𝑃 (𝑃 𝑅) ∧ 𝑄 (𝑃 𝑅)) → 𝑄 (𝑃 𝑅))
49 simp23 1088 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝑃𝑄)
5049necomd 2836 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → 𝑄𝑃)
5126, 10, 11hlatexchb1 33521 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑅𝐴𝑃𝐴) ∧ 𝑄𝑃) → (𝑄 (𝑃 𝑅) ↔ (𝑃 𝑄) = (𝑃 𝑅)))
527, 20, 9, 8, 50, 51syl131anc 1330 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → (𝑄 (𝑃 𝑅) ↔ (𝑃 𝑄) = (𝑃 𝑅)))
5348, 52syl5ib 232 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 (𝑃 𝑅) ∧ 𝑄 (𝑃 𝑅)) → (𝑃 𝑄) = (𝑃 𝑅)))
5447, 53sylbird 248 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) (𝑃 𝑅) → (𝑃 𝑄) = (𝑃 𝑅)))
5554adantr 479 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → ((𝑃 𝑄) (𝑃 𝑅) → (𝑃 𝑄) = (𝑃 𝑅)))
5643, 55syld 45 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → ((𝑃 𝑄) (𝑅 𝑆) → (𝑃 𝑄) = (𝑃 𝑅)))
57563impia 1252 . . . . 5 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅 ∧ (𝑃 𝑄) (𝑅 𝑆)) → (𝑃 𝑄) = (𝑃 𝑅))
5857, 41eqtrd 2643 . . . 4 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅 ∧ (𝑃 𝑄) (𝑅 𝑆)) → (𝑃 𝑄) = (𝑅 𝑆))
59583expia 1258 . . 3 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) ∧ 𝑃𝑅) → ((𝑃 𝑄) (𝑅 𝑆) → (𝑃 𝑄) = (𝑅 𝑆)))
6017, 10, 11hlatjcl 33495 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑆𝐴) → (𝑃 𝑆) ∈ (Base‘𝐾))
617, 8, 23, 60syl3anc 1317 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
6217, 26, 10latjle12 16834 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾))) → ((𝑃 (𝑃 𝑆) ∧ 𝑄 (𝑃 𝑆)) ↔ (𝑃 𝑄) (𝑃 𝑆)))
6316, 19, 22, 61, 62syl13anc 1319 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 (𝑃 𝑆) ∧ 𝑄 (𝑃 𝑆)) ↔ (𝑃 𝑄) (𝑃 𝑆)))
64 simpr 475 . . . . 5 ((𝑃 (𝑃 𝑆) ∧ 𝑄 (𝑃 𝑆)) → 𝑄 (𝑃 𝑆))
6563, 64syl6bir 242 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) (𝑃 𝑆) → 𝑄 (𝑃 𝑆)))
6626, 10, 11hlatexchb1 33521 . . . . 5 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑆𝐴𝑃𝐴) ∧ 𝑄𝑃) → (𝑄 (𝑃 𝑆) ↔ (𝑃 𝑄) = (𝑃 𝑆)))
677, 20, 23, 8, 50, 66syl131anc 1330 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → (𝑄 (𝑃 𝑆) ↔ (𝑃 𝑄) = (𝑃 𝑆)))
6865, 67sylibd 227 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) (𝑃 𝑆) → (𝑃 𝑄) = (𝑃 𝑆)))
695, 59, 68pm2.61ne 2866 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) (𝑅 𝑆) → (𝑃 𝑄) = (𝑅 𝑆)))
7017, 10, 11hlatjcl 33495 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
717, 8, 20, 70syl3anc 1317 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → (𝑃 𝑄) ∈ (Base‘𝐾))
7217, 26latref 16825 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → (𝑃 𝑄) (𝑃 𝑄))
7316, 71, 72syl2anc 690 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → (𝑃 𝑄) (𝑃 𝑄))
74 breq2 4581 . . 3 ((𝑃 𝑄) = (𝑅 𝑆) → ((𝑃 𝑄) (𝑃 𝑄) ↔ (𝑃 𝑄) (𝑅 𝑆)))
7573, 74syl5ibcom 233 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) = (𝑅 𝑆) → (𝑃 𝑄) (𝑅 𝑆)))
7669, 75impbid 200 1 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴𝑆𝐴)) → ((𝑃 𝑄) (𝑅 𝑆) ↔ (𝑃 𝑄) = (𝑅 𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779   class class class wbr 4577  cfv 5790  (class class class)co 6527  Basecbs 15644  lecple 15724  joincjn 16716  Latclat 16817  Atomscatm 33392  HLchlt 33479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-preset 16700  df-poset 16718  df-plt 16730  df-lub 16746  df-glb 16747  df-join 16748  df-meet 16749  df-p0 16811  df-lat 16818  df-covers 33395  df-ats 33396  df-atl 33427  df-cvlat 33451  df-hlat 33480
This theorem is referenced by:  2atjlej  33607  hlatexch3N  33608  hlatexch4  33609  2llnjaN  33694  dalem1  33787  lneq2at  33906  2llnma3r  33916  cdleme11c  34390  cdleme11  34399  cdleme35a  34578  cdleme42k  34614  cdlemg8b  34758  cdlemg13a  34781  cdlemg18b  34809  cdlemg42  34859  trljco  34870
  Copyright terms: Public domain W3C validator