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

Theorem trlord 39032
Description: The ordering of two Hilbert lattice elements (under the fiducial hyperplane 𝑊) is determined by the translations whose traces are under them. (Contributed by NM, 3-Mar-2014.)
Hypotheses
Ref Expression
trlord.b 𝐵 = (Base‘𝐾)
trlord.l = (le‘𝐾)
trlord.a 𝐴 = (Atoms‘𝐾)
trlord.h 𝐻 = (LHyp‘𝐾)
trlord.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlord.r 𝑅 = ((trL‘𝐾)‘𝑊)
Assertion
Ref Expression
trlord (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝑋 𝑌 ↔ ∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌)))
Distinct variable groups:   ,𝑓   𝐵,𝑓   𝑓,𝐻   𝑓,𝐾   𝑅,𝑓   𝑇,𝑓   𝑓,𝑊   𝑓,𝑋   𝑓,𝑌
Allowed substitution hint:   𝐴(𝑓)

Proof of Theorem trlord
Dummy variables 𝑔 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 trlord.b . . . . 5 𝐵 = (Base‘𝐾)
2 trlord.l . . . . 5 = (le‘𝐾)
3 simpl1l 1224 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → 𝐾 ∈ HL)
43hllatd 37826 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → 𝐾 ∈ Lat)
5 simpl1 1191 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
6 simprlr 778 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → 𝑓𝑇)
7 trlord.h . . . . . . 7 𝐻 = (LHyp‘𝐾)
8 trlord.t . . . . . . 7 𝑇 = ((LTrn‘𝐾)‘𝑊)
9 trlord.r . . . . . . 7 𝑅 = ((trL‘𝐾)‘𝑊)
101, 7, 8, 9trlcl 38627 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑓𝑇) → (𝑅𝑓) ∈ 𝐵)
115, 6, 10syl2anc 584 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → (𝑅𝑓) ∈ 𝐵)
12 simpl2l 1226 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → 𝑋𝐵)
13 simpl3l 1228 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → 𝑌𝐵)
14 simprr 771 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → (𝑅𝑓) 𝑋)
15 simprll 777 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → 𝑋 𝑌)
161, 2, 4, 11, 12, 13, 14, 15lattrd 18335 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ ((𝑋 𝑌𝑓𝑇) ∧ (𝑅𝑓) 𝑋)) → (𝑅𝑓) 𝑌)
1716exp44 438 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝑋 𝑌 → (𝑓𝑇 → ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌))))
1817ralrimdv 3149 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝑋 𝑌 → ∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌)))
19 simp11l 1284 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝐾 ∈ HL)
2019hllatd 37826 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝐾 ∈ Lat)
21 simp2r 1200 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝑢𝐴)
22 trlord.a . . . . . . . . . . 11 𝐴 = (Atoms‘𝐾)
231, 22atbase 37751 . . . . . . . . . 10 (𝑢𝐴𝑢𝐵)
2421, 23syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝑢𝐵)
25 simp12l 1286 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝑋𝐵)
26 simp11r 1285 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝑊𝐻)
271, 7lhpbase 38461 . . . . . . . . . 10 (𝑊𝐻𝑊𝐵)
2826, 27syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝑊𝐵)
29 simp3 1138 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝑢 𝑋)
30 simp12r 1287 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝑋 𝑊)
311, 2, 20, 24, 25, 28, 29, 30lattrd 18335 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → 𝑢 𝑊)
3231, 29jca 512 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑋) → (𝑢 𝑊𝑢 𝑋))
33323expia 1121 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴)) → (𝑢 𝑋 → (𝑢 𝑊𝑢 𝑋)))
34 simp11 1203 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → (𝐾 ∈ HL ∧ 𝑊𝐻))
35 simp2r 1200 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → 𝑢𝐴)
36 simp3 1138 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → 𝑢 𝑊)
372, 22, 7, 8, 9cdlemf 39026 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑢𝐴𝑢 𝑊)) → ∃𝑔𝑇 (𝑅𝑔) = 𝑢)
3834, 35, 36, 37syl12anc 835 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → ∃𝑔𝑇 (𝑅𝑔) = 𝑢)
39 simp2l 1199 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → ∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌))
40 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑅𝑓) = (𝑅𝑔))
4140breq1d 5115 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑅𝑓) 𝑋 ↔ (𝑅𝑔) 𝑋))
4240breq1d 5115 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → ((𝑅𝑓) 𝑌 ↔ (𝑅𝑔) 𝑌))
4341, 42imbi12d 344 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ↔ ((𝑅𝑔) 𝑋 → (𝑅𝑔) 𝑌)))
4443rspccv 3578 . . . . . . . . . . . 12 (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) → (𝑔𝑇 → ((𝑅𝑔) 𝑋 → (𝑅𝑔) 𝑌)))
4539, 44syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → (𝑔𝑇 → ((𝑅𝑔) 𝑋 → (𝑅𝑔) 𝑌)))
46 breq1 5108 . . . . . . . . . . . . 13 ((𝑅𝑔) = 𝑢 → ((𝑅𝑔) 𝑋𝑢 𝑋))
47 breq1 5108 . . . . . . . . . . . . 13 ((𝑅𝑔) = 𝑢 → ((𝑅𝑔) 𝑌𝑢 𝑌))
4846, 47imbi12d 344 . . . . . . . . . . . 12 ((𝑅𝑔) = 𝑢 → (((𝑅𝑔) 𝑋 → (𝑅𝑔) 𝑌) ↔ (𝑢 𝑋𝑢 𝑌)))
4948biimpcd 248 . . . . . . . . . . 11 (((𝑅𝑔) 𝑋 → (𝑅𝑔) 𝑌) → ((𝑅𝑔) = 𝑢 → (𝑢 𝑋𝑢 𝑌)))
5045, 49syl6 35 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → (𝑔𝑇 → ((𝑅𝑔) = 𝑢 → (𝑢 𝑋𝑢 𝑌))))
5150rexlimdv 3150 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → (∃𝑔𝑇 (𝑅𝑔) = 𝑢 → (𝑢 𝑋𝑢 𝑌)))
5238, 51mpd 15 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴) ∧ 𝑢 𝑊) → (𝑢 𝑋𝑢 𝑌))
53523expia 1121 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴)) → (𝑢 𝑊 → (𝑢 𝑋𝑢 𝑌)))
5453impd 411 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴)) → ((𝑢 𝑊𝑢 𝑋) → 𝑢 𝑌))
5533, 54syld 47 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) ∧ (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) ∧ 𝑢𝐴)) → (𝑢 𝑋𝑢 𝑌))
5655exp32 421 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) → (𝑢𝐴 → (𝑢 𝑋𝑢 𝑌))))
5756ralrimdv 3149 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) → ∀𝑢𝐴 (𝑢 𝑋𝑢 𝑌)))
58 simp1l 1197 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → 𝐾 ∈ HL)
59 simp2l 1199 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → 𝑋𝐵)
60 simp3l 1201 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → 𝑌𝐵)
611, 2, 22hlatle 37861 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌 ↔ ∀𝑢𝐴 (𝑢 𝑋𝑢 𝑌)))
6258, 59, 60, 61syl3anc 1371 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝑋 𝑌 ↔ ∀𝑢𝐴 (𝑢 𝑋𝑢 𝑌)))
6357, 62sylibrd 258 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌) → 𝑋 𝑌))
6418, 63impbid 211 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵𝑌 𝑊)) → (𝑋 𝑌 ↔ ∀𝑓𝑇 ((𝑅𝑓) 𝑋 → (𝑅𝑓) 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073   class class class wbr 5105  cfv 6496  Basecbs 17083  lecple 17140  Atomscatm 37725  HLchlt 37812  LHypclh 38447  LTrncltrn 38564  trLctrl 38621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-riotaBAD 37415
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-undef 8204  df-map 8767  df-proset 18184  df-poset 18202  df-plt 18219  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-p0 18314  df-p1 18315  df-lat 18321  df-clat 18388  df-oposet 37638  df-ol 37640  df-oml 37641  df-covers 37728  df-ats 37729  df-atl 37760  df-cvlat 37784  df-hlat 37813  df-llines 37961  df-lplanes 37962  df-lvols 37963  df-lines 37964  df-psubsp 37966  df-pmap 37967  df-padd 38259  df-lhyp 38451  df-laut 38452  df-ldil 38567  df-ltrn 38568  df-trl 38622
This theorem is referenced by:  diaord  39510  dihord2pre  39688
  Copyright terms: Public domain W3C validator