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 40075
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 7371 . . . . 5 (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = π‘ž) ∈ V
2 cdlemm10.g . . . . 5 𝐺 = (π‘ž ∈ 𝐢 ↦ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = π‘ž))
31, 2fnmpti 6693 . . . 4 𝐺 Fn 𝐢
4 fvelrnb 6952 . . . 4 (𝐺 Fn 𝐢 β†’ (𝑔 ∈ ran 𝐺 ↔ βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔))
53, 4ax-mp 5 . . 3 (𝑔 ∈ ran 𝐺 ↔ βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔)
6 eqeq2 2744 . . . . . . . . . . . 12 (π‘ž = 𝑠 β†’ ((π‘“β€˜π‘ƒ) = π‘ž ↔ (π‘“β€˜π‘ƒ) = 𝑠))
76riotabidv 7369 . . . . . . . . . . 11 (π‘ž = 𝑠 β†’ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = π‘ž) = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠))
8 riotaex 7371 . . . . . . . . . . 11 (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠) ∈ V
97, 2, 8fvmpt 6998 . . . . . . . . . 10 (𝑠 ∈ 𝐢 β†’ (πΊβ€˜π‘ ) = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠))
10 cdlemm10.f . . . . . . . . . 10 𝐹 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠)
119, 10eqtr4di 2790 . . . . . . . . 9 (𝑠 ∈ 𝐢 β†’ (πΊβ€˜π‘ ) = 𝐹)
1211adantl 482 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ 𝑠 ∈ 𝐢) β†’ (πΊβ€˜π‘ ) = 𝐹)
1312eqeq1d 2734 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ 𝑠 ∈ 𝐢) β†’ ((πΊβ€˜π‘ ) = 𝑔 ↔ 𝐹 = 𝑔))
1413rexbidva 3176 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔 ↔ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔))
15 simpl1 1191 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
16 simprl 769 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑔 ∈ 𝑇)
17 simpl2l 1226 . . . . . . . . . . 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 39097 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) β†’ (π‘”β€˜π‘ƒ) ∈ 𝐴)
2315, 16, 17, 22syl3anc 1371 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ∈ 𝐴)
24 eqid 2732 . . . . . . . . . . . 12 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
25 simpl1l 1224 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝐾 ∈ HL)
2625hllatd 38320 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝐾 ∈ Lat)
2724, 19atbase 38245 . . . . . . . . . . . . . 14 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
2817, 27syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
2924, 20, 21ltrncl 39082 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ 𝑃 ∈ (Baseβ€˜πΎ)) β†’ (π‘”β€˜π‘ƒ) ∈ (Baseβ€˜πΎ))
3015, 16, 28, 29syl3anc 1371 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ∈ (Baseβ€˜πΎ))
31 cdlemm10.j . . . . . . . . . . . . . 14 ∨ = (joinβ€˜πΎ)
3224, 31latjcl 18394 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ (π‘”β€˜π‘ƒ) ∈ (Baseβ€˜πΎ)) β†’ (𝑃 ∨ (π‘”β€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
3326, 28, 30, 32syl3anc 1371 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ (π‘”β€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
34 simpl3l 1228 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑉 ∈ 𝐴)
3524, 31, 19hlatjcl 38323 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ))
3625, 17, 34, 35syl3anc 1371 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ))
3724, 18, 31latlej2 18404 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Baseβ€˜πΎ) ∧ (π‘”β€˜π‘ƒ) ∈ (Baseβ€˜πΎ)) β†’ (π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ (π‘”β€˜π‘ƒ)))
3826, 28, 30, 37syl3anc 1371 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ (π‘”β€˜π‘ƒ)))
39 simpl2 1192 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š))
40 cdlemm10.r . . . . . . . . . . . . . . 15 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
4118, 31, 19, 20, 21, 40trljat1 39123 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (𝑃 ∨ (π‘…β€˜π‘”)) = (𝑃 ∨ (π‘”β€˜π‘ƒ)))
4215, 16, 39, 41syl3anc 1371 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ (π‘…β€˜π‘”)) = (𝑃 ∨ (π‘”β€˜π‘ƒ)))
43 simprr 771 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘…β€˜π‘”) ≀ 𝑉)
4424, 20, 21, 40trlcl 39121 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇) β†’ (π‘…β€˜π‘”) ∈ (Baseβ€˜πΎ))
4515, 16, 44syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘…β€˜π‘”) ∈ (Baseβ€˜πΎ))
4624, 19atbase 38245 . . . . . . . . . . . . . . . 16 (𝑉 ∈ 𝐴 β†’ 𝑉 ∈ (Baseβ€˜πΎ))
4734, 46syl 17 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑉 ∈ (Baseβ€˜πΎ))
4824, 18, 31latjlej2 18409 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ ((π‘…β€˜π‘”) ∈ (Baseβ€˜πΎ) ∧ 𝑉 ∈ (Baseβ€˜πΎ) ∧ 𝑃 ∈ (Baseβ€˜πΎ))) β†’ ((π‘…β€˜π‘”) ≀ 𝑉 β†’ (𝑃 ∨ (π‘…β€˜π‘”)) ≀ (𝑃 ∨ 𝑉)))
4926, 45, 47, 28, 48syl13anc 1372 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ ((π‘…β€˜π‘”) ≀ 𝑉 β†’ (𝑃 ∨ (π‘…β€˜π‘”)) ≀ (𝑃 ∨ 𝑉)))
5043, 49mpd 15 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ (π‘…β€˜π‘”)) ≀ (𝑃 ∨ 𝑉))
5142, 50eqbrtrrd 5172 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (𝑃 ∨ (π‘”β€˜π‘ƒ)) ≀ (𝑃 ∨ 𝑉))
5224, 18, 26, 30, 33, 36, 38, 51lattrd 18401 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉))
5318, 19, 20, 21ltrnel 39096 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ ((π‘”β€˜π‘ƒ) ∈ 𝐴 ∧ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š))
5453simprd 496 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š)
5515, 16, 39, 54syl3anc 1371 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š)
5652, 55jca 512 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ ((π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉) ∧ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š))
57 breq1 5151 . . . . . . . . . . . 12 (π‘Ÿ = (π‘”β€˜π‘ƒ) β†’ (π‘Ÿ ≀ (𝑃 ∨ 𝑉) ↔ (π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉)))
58 breq1 5151 . . . . . . . . . . . . 13 (π‘Ÿ = (π‘”β€˜π‘ƒ) β†’ (π‘Ÿ ≀ π‘Š ↔ (π‘”β€˜π‘ƒ) ≀ π‘Š))
5958notbid 317 . . . . . . . . . . . 12 (π‘Ÿ = (π‘”β€˜π‘ƒ) β†’ (Β¬ π‘Ÿ ≀ π‘Š ↔ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š))
6057, 59anbi12d 631 . . . . . . . . . . 11 (π‘Ÿ = (π‘”β€˜π‘ƒ) β†’ ((π‘Ÿ ≀ (𝑃 ∨ 𝑉) ∧ Β¬ π‘Ÿ ≀ π‘Š) ↔ ((π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉) ∧ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š)))
61 cdlemm10.c . . . . . . . . . . 11 𝐢 = {π‘Ÿ ∈ 𝐴 ∣ (π‘Ÿ ≀ (𝑃 ∨ 𝑉) ∧ Β¬ π‘Ÿ ≀ π‘Š)}
6260, 61elrab2 3686 . . . . . . . . . 10 ((π‘”β€˜π‘ƒ) ∈ 𝐢 ↔ ((π‘”β€˜π‘ƒ) ∈ 𝐴 ∧ ((π‘”β€˜π‘ƒ) ≀ (𝑃 ∨ 𝑉) ∧ Β¬ (π‘”β€˜π‘ƒ) ≀ π‘Š)))
6323, 56, 62sylanbrc 583 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (π‘”β€˜π‘ƒ) ∈ 𝐢)
6418, 19, 20, 21cdlemeiota 39542 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ 𝑔 ∈ 𝑇) β†’ 𝑔 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
6515, 39, 16, 64syl3anc 1371 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ 𝑔 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
6665eqcomd 2738 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)) = 𝑔)
67 eqeq2 2744 . . . . . . . . . . . . 13 (𝑠 = (π‘”β€˜π‘ƒ) β†’ ((π‘“β€˜π‘ƒ) = 𝑠 ↔ (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
6867riotabidv 7369 . . . . . . . . . . . 12 (𝑠 = (π‘”β€˜π‘ƒ) β†’ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = 𝑠) = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
6910, 68eqtrid 2784 . . . . . . . . . . 11 (𝑠 = (π‘”β€˜π‘ƒ) β†’ 𝐹 = (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)))
7069eqeq1d 2734 . . . . . . . . . 10 (𝑠 = (π‘”β€˜π‘ƒ) β†’ (𝐹 = 𝑔 ↔ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)) = 𝑔))
7170rspcev 3612 . . . . . . . . 9 (((π‘”β€˜π‘ƒ) ∈ 𝐢 ∧ (℩𝑓 ∈ 𝑇 (π‘“β€˜π‘ƒ) = (π‘”β€˜π‘ƒ)) = 𝑔) β†’ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔)
7263, 66, 71syl2anc 584 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)) β†’ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔)
7372ex 413 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ((𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉) β†’ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔))
74 breq1 5151 . . . . . . . . . . . . 13 (π‘Ÿ = 𝑠 β†’ (π‘Ÿ ≀ (𝑃 ∨ 𝑉) ↔ 𝑠 ≀ (𝑃 ∨ 𝑉)))
75 breq1 5151 . . . . . . . . . . . . . 14 (π‘Ÿ = 𝑠 β†’ (π‘Ÿ ≀ π‘Š ↔ 𝑠 ≀ π‘Š))
7675notbid 317 . . . . . . . . . . . . 13 (π‘Ÿ = 𝑠 β†’ (Β¬ π‘Ÿ ≀ π‘Š ↔ Β¬ 𝑠 ≀ π‘Š))
7774, 76anbi12d 631 . . . . . . . . . . . 12 (π‘Ÿ = 𝑠 β†’ ((π‘Ÿ ≀ (𝑃 ∨ 𝑉) ∧ Β¬ π‘Ÿ ≀ π‘Š) ↔ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)))
7877, 61elrab2 3686 . . . . . . . . . . 11 (𝑠 ∈ 𝐢 ↔ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)))
79 simpl1 1191 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
80 simpl2l 1226 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑃 ∈ 𝐴)
81 simpl2r 1227 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ Β¬ 𝑃 ≀ π‘Š)
82 simprl 769 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑠 ∈ 𝐴)
83 simprrr 780 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ Β¬ 𝑠 ≀ π‘Š)
8418, 19, 20, 21, 10ltrniotacl 39536 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑠 ∈ 𝐴 ∧ Β¬ 𝑠 ≀ π‘Š)) β†’ 𝐹 ∈ 𝑇)
8518, 19, 20, 21, 10ltrniotaval 39538 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑠 ∈ 𝐴 ∧ Β¬ 𝑠 ≀ π‘Š)) β†’ (πΉβ€˜π‘ƒ) = 𝑠)
8684, 85jca 512 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑠 ∈ 𝐴 ∧ Β¬ 𝑠 ≀ π‘Š)) β†’ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠))
8779, 80, 81, 82, 83, 86syl122anc 1379 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠))
88 simp3l 1201 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ 𝐹 ∈ 𝑇)
89 simp11 1203 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
90 simp12 1204 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š))
91 eqid 2732 . . . . . . . . . . . . . . . . 17 (meetβ€˜πΎ) = (meetβ€˜πΎ)
9218, 31, 91, 19, 20, 21, 40trlval2 39120 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
9389, 88, 90, 92syl3anc 1371 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
94 simp3r 1202 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (πΉβ€˜π‘ƒ) = 𝑠)
9594oveq2d 7427 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (𝑃 ∨ (πΉβ€˜π‘ƒ)) = (𝑃 ∨ 𝑠))
9695oveq1d 7426 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š) = ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š))
9793, 96eqtrd 2772 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š))
98 simpl1l 1224 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝐾 ∈ HL)
99 simpl3l 1228 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑉 ∈ 𝐴)
10018, 31, 19hlatlej1 38331 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ 𝑃 ≀ (𝑃 ∨ 𝑉))
10198, 80, 99, 100syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑃 ≀ (𝑃 ∨ 𝑉))
102 simprrl 779 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑠 ≀ (𝑃 ∨ 𝑉))
10398hllatd 38320 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝐾 ∈ Lat)
10480, 27syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
10524, 19atbase 38245 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ 𝐴 β†’ 𝑠 ∈ (Baseβ€˜πΎ))
106105ad2antrl 726 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ 𝑠 ∈ (Baseβ€˜πΎ))
10798, 80, 99, 35syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ))
10824, 18, 31latjle12 18405 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ 𝑠 ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑉) ∧ 𝑠 ≀ (𝑃 ∨ 𝑉)) ↔ (𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉)))
109103, 104, 106, 107, 108syl13anc 1372 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ≀ (𝑃 ∨ 𝑉) ∧ 𝑠 ≀ (𝑃 ∨ 𝑉)) ↔ (𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉)))
110101, 102, 109mpbi2and 710 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉))
11124, 31, 19hlatjcl 38323 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ (𝑃 ∨ 𝑠) ∈ (Baseβ€˜πΎ))
11298, 80, 82, 111syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝑃 ∨ 𝑠) ∈ (Baseβ€˜πΎ))
113 simpl1r 1225 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ π‘Š ∈ 𝐻)
11424, 20lhpbase 38955 . . . . . . . . . . . . . . . . . . 19 (π‘Š ∈ 𝐻 β†’ π‘Š ∈ (Baseβ€˜πΎ))
115113, 114syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ π‘Š ∈ (Baseβ€˜πΎ))
11624, 18, 91latmlem1 18424 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ ((𝑃 ∨ 𝑠) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ 𝑉) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š)))
117103, 112, 107, 115, 116syl13anc 1372 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑠) ≀ (𝑃 ∨ 𝑉) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š)))
118110, 117mpd 15 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š))
11918, 31, 91, 19, 20lhpat4N 39001 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š) = 𝑉)
120119adantr 481 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑉)(meetβ€˜πΎ)π‘Š) = 𝑉)
121118, 120breqtrd 5174 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ 𝑉)
1221213adant3 1132 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ ((𝑃 ∨ 𝑠)(meetβ€˜πΎ)π‘Š) ≀ 𝑉)
12397, 122eqbrtrd 5170 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (π‘…β€˜πΉ) ≀ 𝑉)
12488, 123jca 512 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š)) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) = 𝑠)) β†’ (𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉))
12587, 124mpd3an3 1462 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ (𝑠 ∈ 𝐴 ∧ (𝑠 ≀ (𝑃 ∨ 𝑉) ∧ Β¬ 𝑠 ≀ π‘Š))) β†’ (𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉))
12678, 125sylan2b 594 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) ∧ 𝑠 ∈ 𝐢) β†’ (𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉))
127126ex 413 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (𝑠 ∈ 𝐢 β†’ (𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉)))
128 eleq1 2821 . . . . . . . . . . 11 (𝐹 = 𝑔 β†’ (𝐹 ∈ 𝑇 ↔ 𝑔 ∈ 𝑇))
129 fveq2 6891 . . . . . . . . . . . 12 (𝐹 = 𝑔 β†’ (π‘…β€˜πΉ) = (π‘…β€˜π‘”))
130129breq1d 5158 . . . . . . . . . . 11 (𝐹 = 𝑔 β†’ ((π‘…β€˜πΉ) ≀ 𝑉 ↔ (π‘…β€˜π‘”) ≀ 𝑉))
131128, 130anbi12d 631 . . . . . . . . . 10 (𝐹 = 𝑔 β†’ ((𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉) ↔ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)))
132131biimpcd 248 . . . . . . . . 9 ((𝐹 ∈ 𝑇 ∧ (π‘…β€˜πΉ) ≀ 𝑉) β†’ (𝐹 = 𝑔 β†’ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)))
133127, 132syl6 35 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (𝑠 ∈ 𝐢 β†’ (𝐹 = 𝑔 β†’ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉))))
134133rexlimdv 3153 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔 β†’ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)))
13573, 134impbid 211 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ((𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉) ↔ βˆƒπ‘  ∈ 𝐢 𝐹 = 𝑔))
13614, 135bitr4d 281 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔 ↔ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉)))
137 fveq2 6891 . . . . . . 7 (𝑓 = 𝑔 β†’ (π‘…β€˜π‘“) = (π‘…β€˜π‘”))
138137breq1d 5158 . . . . . 6 (𝑓 = 𝑔 β†’ ((π‘…β€˜π‘“) ≀ 𝑉 ↔ (π‘…β€˜π‘”) ≀ 𝑉))
139138elrab 3683 . . . . 5 (𝑔 ∈ {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉} ↔ (𝑔 ∈ 𝑇 ∧ (π‘…β€˜π‘”) ≀ 𝑉))
140136, 139bitr4di 288 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔 ↔ 𝑔 ∈ {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉}))
141 simp1l 1197 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ 𝐾 ∈ HL)
142 simp1r 1198 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ π‘Š ∈ 𝐻)
143 simp3l 1201 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ 𝑉 ∈ 𝐴)
144143, 46syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ 𝑉 ∈ (Baseβ€˜πΎ))
145 simp3r 1202 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ 𝑉 ≀ π‘Š)
146 cdlemm10.i . . . . . . 7 𝐼 = ((DIsoAβ€˜πΎ)β€˜π‘Š)
14724, 18, 20, 21, 40, 146diaval 39989 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑉 ∈ (Baseβ€˜πΎ) ∧ 𝑉 ≀ π‘Š)) β†’ (πΌβ€˜π‘‰) = {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉})
148141, 142, 144, 145, 147syl22anc 837 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (πΌβ€˜π‘‰) = {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉})
149148eleq2d 2819 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (𝑔 ∈ (πΌβ€˜π‘‰) ↔ 𝑔 ∈ {𝑓 ∈ 𝑇 ∣ (π‘…β€˜π‘“) ≀ 𝑉}))
150140, 149bitr4d 281 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (βˆƒπ‘  ∈ 𝐢 (πΊβ€˜π‘ ) = 𝑔 ↔ 𝑔 ∈ (πΌβ€˜π‘‰)))
1515, 150bitrid 282 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ (𝑔 ∈ ran 𝐺 ↔ 𝑔 ∈ (πΌβ€˜π‘‰)))
152151eqrdv 2730 1 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š)) β†’ ran 𝐺 = (πΌβ€˜π‘‰))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3070  {crab 3432   class class class wbr 5148   ↦ cmpt 5231  ran crn 5677   Fn wfn 6538  β€˜cfv 6543  β„©crio 7366  (class class class)co 7411  Basecbs 17146  lecple 17206  joincjn 18266  meetcmee 18267  Latclat 18386  Atomscatm 38219  HLchlt 38306  LHypclh 38941  LTrncltrn 39058  trLctrl 39115  DIsoAcdia 39985
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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-riotaBAD 37909
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-undef 8260  df-map 8824  df-proset 18250  df-poset 18268  df-plt 18285  df-lub 18301  df-glb 18302  df-join 18303  df-meet 18304  df-p0 18380  df-p1 18381  df-lat 18387  df-clat 18454  df-oposet 38132  df-ol 38134  df-oml 38135  df-covers 38222  df-ats 38223  df-atl 38254  df-cvlat 38278  df-hlat 38307  df-llines 38455  df-lplanes 38456  df-lvols 38457  df-lines 38458  df-psubsp 38460  df-pmap 38461  df-padd 38753  df-lhyp 38945  df-laut 38946  df-ldil 39061  df-ltrn 39062  df-trl 39116  df-disoa 39986
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator