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

Theorem cdlemm10N 39989
Description: The image of the map 𝐺 is the entire one-dimensional subspace (πΌβ€˜π‘‰). Remark after Lemma M of [Crawley] p. 121 line 23. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdlemm10.l ≀ = (leβ€˜πΎ)
cdlemm10.j ∨ = (joinβ€˜πΎ)
cdlemm10.a 𝐴 = (Atomsβ€˜πΎ)
cdlemm10.h 𝐻 = (LHypβ€˜πΎ)
cdlemm10.t 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
cdlemm10.r 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
cdlemm10.i 𝐼 = ((DIsoAβ€˜πΎ)β€˜π‘Š)
cdlemm10.c 𝐢 = {π‘Ÿ ∈ 𝐴 ∣ (π‘Ÿ ≀ (𝑃 ∨ 𝑉) ∧ Β¬ π‘Ÿ ≀ π‘Š)}
cdlemm10.f 𝐹 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠)
cdlemm10.g 𝐺 = (π‘ž ∈ 𝐢 ↦ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = π‘ž))
Assertion
Ref Expression
cdlemm10N (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ran 𝐺 = (πΌβ€˜π‘‰))
Distinct variable groups:   𝑓,π‘Ÿ,𝑠, ≀   ∨ ,π‘Ÿ   𝐴,𝑓,π‘Ÿ,𝑠   𝑠,π‘ž,𝐢   𝐺,𝑠   𝑓,𝐻,𝑠   𝑓,𝐾,𝑠   𝑓,π‘ž,𝑃,π‘Ÿ,𝑠   𝑅,𝑓,𝑠   𝑇,𝑓,π‘ž,𝑠   𝑓,𝑉,π‘Ÿ,𝑠   𝑓,π‘Š,π‘Ÿ,𝑠
Allowed substitution hints:   𝐴(π‘ž)   𝐢(𝑓,π‘Ÿ)   𝑅(π‘Ÿ,π‘ž)   𝑇(π‘Ÿ)   𝐹(𝑓,𝑠,π‘Ÿ,π‘ž)   𝐺(𝑓,π‘Ÿ,π‘ž)   𝐻(π‘Ÿ,π‘ž)   𝐼(𝑓,𝑠,π‘Ÿ,π‘ž)   ∨ (𝑓,𝑠,π‘ž)   𝐾(π‘Ÿ,π‘ž)   ≀ (π‘ž)   𝑉(π‘ž)   π‘Š(π‘ž)

Proof of Theorem cdlemm10N
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 riotaex 7369 . . . . 5 (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = π‘ž) ∈ V
2 cdlemm10.g . . . . 5 𝐺 = (π‘ž ∈ 𝐢 ↦ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = π‘ž))
31, 2fnmpti 6694 . . . 4 𝐺 Fn 𝐢
4 fvelrnb 6953 . . . 4 (𝐺 Fn 𝐢 β†’ (𝑔 ∈ ran 𝐺 ↔ βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔))
53, 4ax-mp 5 . . 3 (𝑔 ∈ ran 𝐺 ↔ βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔)
6 eqeq2 2745 . . . . . . . . . . . 12 (π‘ž = 𝑠 β†’ ((π‘“β€˜π‘ƒ) = π‘ž ↔ (π‘“β€˜π‘ƒ) = 𝑠))
76riotabidv 7367 . . . . . . . . . . 11 (π‘ž = 𝑠 β†’ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = π‘ž) = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠))
8 riotaex 7369 . . . . . . . . . . 11 (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠) ∈ V
97, 2, 8fvmpt 6999 . . . . . . . . . 10 (𝑠 ∈ 𝐢 β†’ (πΊβ€˜π‘ ) = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠))
10 cdlemm10.f . . . . . . . . . 10 𝐹 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠)
119, 10eqtr4di 2791 . . . . . . . . 9 (𝑠 ∈ 𝐢 β†’ (πΊβ€˜π‘ ) = 𝐹)
1211adantl 483 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ 𝑠 ∈ 𝐢) β†’ (πΊβ€˜π‘ ) = 𝐹)
1312eqeq1d 2735 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ 𝑠 ∈ 𝐢) β†’ ((πΊβ€˜π‘ ) = 𝑔 ↔ 𝐹 = 𝑔))
1413rexbidva 3177 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔 ↔ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔))
15 simpl1 1192 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
16 simprl 770 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑔 ∈ 𝑇)
17 simpl2l 1227 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑃 ∈ 𝐴)
18 cdlemm10.l . . . . . . . . . . . 12 ≀ = (leβ€˜πΎ)
19 cdlemm10.a . . . . . . . . . . . 12 𝐴 = (Atomsβ€˜πΎ)
20 cdlemm10.h . . . . . . . . . . . 12 𝐻 = (LHypβ€˜πΎ)
21 cdlemm10.t . . . . . . . . . . . 12 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
2218, 19, 20, 21ltrnat 39011 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) β†’ (π‘”β€˜π‘ƒ) ∈ 𝐴)
2315, 16, 17, 22syl3anc 1372 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ∈ 𝐴)
24 eqid 2733 . . . . . . . . . . . 12 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
25 simpl1l 1225 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝐾 ∈ HL)
2625hllatd 38234 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝐾 ∈ Lat)
2724, 19atbase 38159 . . . . . . . . . . . . . 14 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
2817, 27syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
2924, 20, 21ltrncl 38996 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ 𝑃 ∈ (Baseβ€˜πΎ)) β†’ (π‘”β€˜π‘ƒ) ∈ (Baseβ€˜πΎ))
3015, 16, 28, 29syl3anc 1372 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ∈ (Baseβ€˜πΎ))
31 cdlemm10.j . . . . . . . . . . . . . 14 ∨ = (joinβ€˜πΎ)
3224, 31latjcl 18392 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ (π‘”β€˜π‘ƒ) ∈ (Baseβ€˜πΎ)) β†’ (𝑃 ∨ (π‘”β€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
3326, 28, 30, 32syl3anc 1372 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ (π‘”β€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
34 simpl3l 1229 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑉 ∈ 𝐴)
3524, 31, 19hlatjcl 38237 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ))
3625, 17, 34, 35syl3anc 1372 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ))
3724, 18, 31latlej2 18402 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ (π‘”β€˜π‘ƒ) ∈ (Baseβ€˜πΎ)) β†’ (π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ (π‘”β€˜π‘ƒ)))
3826, 28, 30, 37syl3anc 1372 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ (π‘”β€˜π‘ƒ)))
39 simpl2 1193 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š))
40 cdlemm10.r . . . . . . . . . . . . . . 15 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
4118, 31, 19, 20, 21, 40trljat1 39037 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (𝑃 ∨ (π‘…β€˜π‘”)) = (𝑃 ∨ (π‘”β€˜π‘ƒ)))
4215, 16, 39, 41syl3anc 1372 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ (π‘…β€˜π‘”)) = (𝑃 ∨ (π‘”β€˜π‘ƒ)))
43 simprr 772 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘…β€˜π‘”) ≀ 𝑉)
4424, 20, 21, 40trlcl 39035 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇) β†’ (π‘…β€˜π‘”) ∈ (Baseβ€˜πΎ))
4515, 16, 44syl2anc 585 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘…β€˜π‘”) ∈ (Baseβ€˜πΎ))
4624, 19atbase 38159 . . . . . . . . . . . . . . . 16 (𝑉 ∈ 𝐴 β†’ 𝑉 ∈ (Baseβ€˜πΎ))
4734, 46syl 17 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑉 ∈ (Baseβ€˜πΎ))
4824, 18, 31latjlej2 18407 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ ((π‘…β€˜π‘”) ∈ (Baseβ€˜πΎ) ∧ 𝑉 ∈ (Baseβ€˜πΎ) ∧ 𝑃 ∈ (Baseβ€˜πΎ))) β†’ ((π‘…β€˜π‘”) ≀ 𝑉 β†’ (𝑃 ∨ (π‘…β€˜π‘”)) ≀ (𝑃 ∨ 𝑉)))
4926, 45, 47, 28, 48syl13anc 1373 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ ((π‘…β€˜π‘”) ≀ 𝑉 β†’ (𝑃 ∨ (π‘…β€˜π‘”)) ≀ (𝑃 ∨ 𝑉)))
5043, 49mpd 15 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ (π‘…β€˜π‘”)) ≀ (𝑃 ∨ 𝑉))
5142, 50eqbrtrrd 5173 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ (π‘”β€˜π‘ƒ)) ≀ (𝑃 ∨ 𝑉))
5224, 18, 26, 30, 33, 36, 38, 51lattrd 18399 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉))
5318, 19, 20, 21ltrnel 39010 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ ((π‘”β€˜π‘ƒ) ∈ 𝐴 ∧ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š))
5453simprd 497 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š)
5515, 16, 39, 54syl3anc 1372 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š)
5652, 55jca 513 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ ((π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉) ∧ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š))
57 breq1 5152 . . . . . . . . . . . 12 (π‘Ÿ = (π‘”β€˜π‘ƒ) β†’ (π‘Ÿ ≀ (𝑃 ∨ 𝑉) ↔ (π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉)))
58 breq1 5152 . . . . . . . . . . . . 13 (π‘Ÿ = (π‘”β€˜π‘ƒ) β†’ (π‘Ÿ ≀ π‘Š ↔ (π‘”β€˜π‘ƒ) ≀ π‘Š))
5958notbid 318 . . . . . . . . . . . 12 (π‘Ÿ = (π‘”β€˜π‘ƒ) β†’ (Β¬ π‘Ÿ ≀ π‘Š ↔ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š))
6057, 59anbi12d 632 . . . . . . . . . . 11 (π‘Ÿ = (π‘”β€˜π‘ƒ) β†’ ((π‘Ÿ ≀ (𝑃 ∨ 𝑉) ∧ Β¬ π‘Ÿ ≀ π‘Š) ↔ ((π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉) ∧ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š)))
61 cdlemm10.c . . . . . . . . . . 11 𝐢 = {π‘Ÿ ∈ 𝐴 ∣ (π‘Ÿ ≀ (𝑃 ∨ 𝑉) ∧ Β¬ π‘Ÿ ≀ π‘Š)}
6260, 61elrab2 3687 . . . . . . . . . 10 ((π‘”β€˜π‘ƒ) ∈ 𝐢 ↔ ((π‘”β€˜π‘ƒ) ∈ 𝐴 ∧ ((π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉) ∧ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š)))
6323, 56, 62sylanbrc 584 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ∈ 𝐢)
6418, 19, 20, 21cdlemeiota 39456 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ 𝑔 ∈ 𝑇) β†’ 𝑔 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
6515, 39, 16, 64syl3anc 1372 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑔 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
6665eqcomd 2739 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)) = 𝑔)
67 eqeq2 2745 . . . . . . . . . . . . 13 (𝑠 = (π‘”β€˜π‘ƒ) β†’ ((π‘“β€˜π‘ƒ) = 𝑠 ↔ (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
6867riotabidv 7367 . . . . . . . . . . . 12 (𝑠 = (π‘”β€˜π‘ƒ) β†’ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠) = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
6910, 68eqtrid 2785 . . . . . . . . . . 11 (𝑠 = (π‘”β€˜π‘ƒ) β†’ 𝐹 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
7069eqeq1d 2735 . . . . . . . . . 10 (𝑠 = (π‘”β€˜π‘ƒ) β†’ (𝐹 = 𝑔 ↔ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)) = 𝑔))
7170rspcev 3613 . . . . . . . . 9 (((π‘”β€˜π‘ƒ) ∈ 𝐢 ∧ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)) = 𝑔) β†’ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔)
7263, 66, 71syl2anc 585 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔)
7372ex 414 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ((𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉) β†’ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔))
74 breq1 5152 . . . . . . . . . . . . 13 (π‘Ÿ = 𝑠 β†’ (π‘Ÿ ≀ (𝑃 ∨ 𝑉) ↔ 𝑠 ≀ (𝑃 ∨ 𝑉)))
75 breq1 5152 . . . . . . . . . . . . . 14 (π‘Ÿ = 𝑠 β†’ (π‘Ÿ ≀ π‘Š ↔ 𝑠 ≀ π‘Š))
7675notbid 318 . . . . . . . . . . . . 13 (π‘Ÿ = 𝑠 β†’ (Β¬ π‘Ÿ ≀ π‘Š ↔ Β¬ 𝑠 ≀ π‘Š))
7774, 76anbi12d 632 . . . . . . . . . . . 12 (π‘Ÿ = 𝑠 β†’ ((π‘Ÿ ≀ (𝑃 ∨ 𝑉) ∧ Β¬ π‘Ÿ ≀ π‘Š) ↔ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)))
7877, 61elrab2 3687 . . . . . . . . . . 11 (𝑠 ∈ 𝐢 ↔ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)))
79 simpl1 1192 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
80 simpl2l 1227 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑃 ∈ 𝐴)
81 simpl2r 1228 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ Β¬ 𝑃 ≀ π‘Š)
82 simprl 770 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑠 ∈ 𝐴)
83 simprrr 781 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ Β¬ 𝑠 ≀ π‘Š)
8418, 19, 20, 21, 10ltrniotacl 39450 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑠 ∈ 𝐴 ∧ Β¬ 𝑠 ≀ π‘Š)) β†’ 𝐹 ∈ 𝑇)
8518, 19, 20, 21, 10ltrniotaval 39452 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑠 ∈ 𝐴 ∧ Β¬ 𝑠 ≀ π‘Š)) β†’ (πΉβ€˜π‘ƒ) = 𝑠)
8684, 85jca 513 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑠 ∈ 𝐴 ∧ Β¬ 𝑠 ≀ π‘Š)) β†’ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠))
8779, 80, 81, 82, 83, 86syl122anc 1380 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠))
88 simp3l 1202 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ 𝐹 ∈ 𝑇)
89 simp11 1204 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
90 simp12 1205 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š))
91 eqid 2733 . . . . . . . . . . . . . . . . 17 (meetβ€˜πΎ) = (meetβ€˜πΎ)
9218, 31, 91, 19, 20, 21, 40trlval2 39034 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
9389, 88, 90, 92syl3anc 1372 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
94 simp3r 1203 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (πΉβ€˜π‘ƒ) = 𝑠)
9594oveq2d 7425 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (𝑃 ∨ (πΉβ€˜π‘ƒ)) = (𝑃 ∨ 𝑠))
9695oveq1d 7424 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š) = ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š))
9793, 96eqtrd 2773 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š))
98 simpl1l 1225 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝐾 ∈ HL)
99 simpl3l 1229 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑉 ∈ 𝐴)
10018, 31, 19hlatlej1 38245 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ 𝑃 ≀ (𝑃 ∨ 𝑉))
10198, 80, 99, 100syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑃 ≀ (𝑃 ∨ 𝑉))
102 simprrl 780 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑠 ≀ (𝑃 ∨ 𝑉))
10398hllatd 38234 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝐾 ∈ Lat)
10480, 27syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
10524, 19atbase 38159 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ 𝐴 β†’ 𝑠 ∈ (Baseβ€˜πΎ))
106105ad2antrl 727 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑠 ∈ (Baseβ€˜πΎ))
10798, 80, 99, 35syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ))
10824, 18, 31latjle12 18403 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑠 ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑉) ∧ 𝑠 ≀ (𝑃 ∨ 𝑉)) ↔ (𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉)))
109103, 104, 106, 107, 108syl13anc 1373 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑉) ∧ 𝑠 ≀ (𝑃 ∨ 𝑉)) ↔ (𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉)))
110101, 102, 109mpbi2and 711 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉))
11124, 31, 19hlatjcl 38237 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ (𝑃 ∨ 𝑠) ∈ (Baseβ€˜πΎ))
11298, 80, 82, 111syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑠) ∈ (Baseβ€˜πΎ))
113 simpl1r 1226 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ π‘Š ∈ 𝐻)
11424, 20lhpbase 38869 . . . . . . . . . . . . . . . . . . 19 (π‘Š ∈ 𝐻 β†’ π‘Š ∈ (Baseβ€˜πΎ))
115113, 114syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ π‘Š ∈ (Baseβ€˜πΎ))
11624, 18, 91latmlem1 18422 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑠) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š)))
117103, 112, 107, 115, 116syl13anc 1373 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š)))
118110, 117mpd 15 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š))
11918, 31, 91, 19, 20lhpat4N 38915 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š) = 𝑉)
120119adantr 482 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š) = 𝑉)
121118, 120breqtrd 5175 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ 𝑉)
1221213adant3 1133 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ 𝑉)
12397, 122eqbrtrd 5171 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (π‘…β€˜πΉ) ≀ 𝑉)
12488, 123jca 513 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉))
12587, 124mpd3an3 1463 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉))
12678, 125sylan2b 595 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ 𝑠 ∈ 𝐢) β†’ (𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉))
127126ex 414 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (𝑠 ∈ 𝐢 β†’ (𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉)))
128 eleq1 2822 . . . . . . . . . . 11 (𝐹 = 𝑔 β†’ (𝐹 ∈ 𝑇 ↔ 𝑔 ∈ 𝑇))
129 fveq2 6892 . . . . . . . . . . . 12 (𝐹 = 𝑔 β†’ (π‘…β€˜πΉ) = (π‘…β€˜π‘”))
130129breq1d 5159 . . . . . . . . . . 11 (𝐹 = 𝑔 β†’ ((π‘…β€˜πΉ) ≀ 𝑉 ↔ (π‘…β€˜π‘”) ≀ 𝑉))
131128, 130anbi12d 632 . . . . . . . . . 10 (𝐹 = 𝑔 β†’ ((𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉) ↔ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)))
132131biimpcd 248 . . . . . . . . 9 ((𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉) β†’ (𝐹 = 𝑔 β†’ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)))
133127, 132syl6 35 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (𝑠 ∈ 𝐢 β†’ (𝐹 = 𝑔 β†’ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉))))
134133rexlimdv 3154 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔 β†’ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)))
13573, 134impbid 211 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ((𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉) ↔ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔))
13614, 135bitr4d 282 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔 ↔ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)))
137 fveq2 6892 . . . . . . 7 (𝑓 = 𝑔 β†’ (π‘…β€˜π‘“) = (π‘…β€˜π‘”))
138137breq1d 5159 . . . . . 6 (𝑓 = 𝑔 β†’ ((π‘…β€˜π‘“) ≀ 𝑉 ↔ (π‘…β€˜π‘”) ≀ 𝑉))
139138elrab 3684 . . . . 5 (𝑔 ∈ {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉} ↔ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉))
140136, 139bitr4di 289 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔 ↔ 𝑔 ∈ {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉}))
141 simp1l 1198 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ 𝐾 ∈ HL)
142 simp1r 1199 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ π‘Š ∈ 𝐻)
143 simp3l 1202 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ 𝑉 ∈ 𝐴)
144143, 46syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ 𝑉 ∈ (Baseβ€˜πΎ))
145 simp3r 1203 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ 𝑉 ≀ π‘Š)
146 cdlemm10.i . . . . . . 7 𝐼 = ((DIsoAβ€˜πΎ)β€˜π‘Š)
14724, 18, 20, 21, 40, 146diaval 39903 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑉 ∈ (Baseβ€˜πΎ) ∧ 𝑉 ≀ π‘Š)) β†’ (πΌβ€˜π‘‰) = {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉})
148141, 142, 144, 145, 147syl22anc 838 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (πΌβ€˜π‘‰) = {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉})
149148eleq2d 2820 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (𝑔 ∈ (πΌβ€˜π‘‰) ↔ 𝑔 ∈ {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉}))
150140, 149bitr4d 282 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔 ↔ 𝑔 ∈ (πΌβ€˜π‘‰)))
1515, 150bitrid 283 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (𝑔 ∈ ran 𝐺 ↔ 𝑔 ∈ (πΌβ€˜π‘‰)))
152151eqrdv 2731 1 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ran 𝐺 = (πΌβ€˜π‘‰))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆƒwrex 3071  {crab 3433   class class class wbr 5149   ↦ cmpt 5232  ran crn 5678   Fn wfn 6539  β€˜cfv 6544  β„©crio 7364  (class class class)co 7409  Basecbs 17144  lecple 17204  joincjn 18264  meetcmee 18265  Latclat 18384  Atomscatm 38133  HLchlt 38220  LHypclh 38855  LTrncltrn 38972  trLctrl 39029  DIsoAcdia 39899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-riotaBAD 37823
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-undef 8258  df-map 8822  df-proset 18248  df-poset 18266  df-plt 18283  df-lub 18299  df-glb 18300  df-join 18301  df-meet 18302  df-p0 18378  df-p1 18379  df-lat 18385  df-clat 18452  df-oposet 38046  df-ol 38048  df-oml 38049  df-covers 38136  df-ats 38137  df-atl 38168  df-cvlat 38192  df-hlat 38221  df-llines 38369  df-lplanes 38370  df-lvols 38371  df-lines 38372  df-psubsp 38374  df-pmap 38375  df-padd 38667  df-lhyp 38859  df-laut 38860  df-ldil 38975  df-ltrn 38976  df-trl 39030  df-disoa 39900
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator