MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lubun Structured version   Visualization version   GIF version
Theorem lubun 18468
Description: The LUB of a union. (Contributed by NM, 5-Mar-2012.)
Hypotheses
Ref Expression
lubun.b 𝐡 = (Baseβ€˜πΎ)
lubun.j ∨ = (joinβ€˜πΎ)
lubun.u π‘ˆ = (lubβ€˜πΎ)
Assertion
Ref Expression
lubun ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜(𝑆 βˆͺ 𝑇)) = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
Proof of Theorem lubun
Dummy variables π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lubun.b . . 3 𝐡 = (Baseβ€˜πΎ)
2 eqid 2733 . . 3 (leβ€˜πΎ) = (leβ€˜πΎ)
3 lubun.u . . 3 π‘ˆ = (lubβ€˜πΎ)
4 biid 261 . . 3 ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) ↔ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)))
5 simp1 1137 . . 3 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ 𝐾 ∈ CLat)
6 unss 4185 . . . . 5 ((𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ↔ (𝑆 βˆͺ 𝑇) βŠ† 𝐡)
76biimpi 215 . . . 4 ((𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (𝑆 βˆͺ 𝑇) βŠ† 𝐡)
873adant1 1131 . . 3 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (𝑆 βˆͺ 𝑇) βŠ† 𝐡)
91, 2, 3, 4, 5, 8lubval 18309 . 2 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜(𝑆 βˆͺ 𝑇)) = (β„©π‘₯ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))))
10 clatl 18461 . . . . 5 (𝐾 ∈ CLat β†’ 𝐾 ∈ Lat)
11103ad2ant1 1134 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ 𝐾 ∈ Lat)
121, 3clatlubcl 18456 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
13123adant3 1133 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
141, 3clatlubcl 18456 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
15143adant2 1132 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
16 lubun.j . . . . 5 ∨ = (joinβ€˜πΎ)
171, 16latjcl 18392 . . . 4 ((𝐾 ∈ Lat ∧ (π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
1811, 13, 15, 17syl3anc 1372 . . 3 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
19 simpl1 1192 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝐾 ∈ CLat)
2019, 10syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝐾 ∈ Lat)
21 simpl2 1193 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑆 βŠ† 𝐡)
22 simpr 486 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 ∈ 𝑆)
2321, 22sseldd 3984 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 ∈ 𝐡)
2419, 21, 12syl2anc 585 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
25 simpl3 1194 . . . . . . . . . . . . . 14 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑇 βŠ† 𝐡)
2619, 25, 14syl2anc 585 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
2720, 24, 26, 17syl3anc 1372 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
281, 2, 3lubel 18467 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑦 ∈ 𝑆 ∧ 𝑆 βŠ† 𝐡) β†’ 𝑦(leβ€˜πΎ)(π‘ˆβ€˜π‘†))
2919, 22, 21, 28syl3anc 1372 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦(leβ€˜πΎ)(π‘ˆβ€˜π‘†))
301, 2, 16latlej1 18401 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡) β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
3120, 24, 26, 30syl3anc 1372 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
321, 2, 20, 23, 24, 27, 29, 31lattrd 18399 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
3332ralrimiva 3147 . . . . . . . . . 10 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
3411adantr 482 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝐾 ∈ Lat)
35 simpl3 1194 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑇 βŠ† 𝐡)
36 simpr 486 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑦 ∈ 𝑇)
3735, 36sseldd 3984 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑦 ∈ 𝐡)
38 simpl1 1192 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝐾 ∈ CLat)
3938, 35, 14syl2anc 585 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
4018adantr 482 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
411, 2, 3lubel 18467 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑦 ∈ 𝑇 ∧ 𝑇 βŠ† 𝐡) β†’ 𝑦(leβ€˜πΎ)(π‘ˆβ€˜π‘‡))
4238, 36, 35, 41syl3anc 1372 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑦(leβ€˜πΎ)(π‘ˆβ€˜π‘‡))
43 simpl2 1193 . . . . . . . . . . . . . 14 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑆 βŠ† 𝐡)
4438, 43, 12syl2anc 585 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
451, 2, 16latlej2 18402 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡) β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
4634, 44, 39, 45syl3anc 1372 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
471, 2, 34, 37, 39, 40, 42, 46lattrd 18399 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
4847ralrimiva 3147 . . . . . . . . . 10 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
49 ralunb 4192 . . . . . . . . . 10 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ↔ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
5033, 48, 49sylanbrc 584 . . . . . . . . 9 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
51 breq2 5153 . . . . . . . . . . . . 13 (𝑧 = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (𝑦(leβ€˜πΎ)𝑧 ↔ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
5251ralbidv 3178 . . . . . . . . . . . 12 (𝑧 = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 ↔ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
53 breq2 5153 . . . . . . . . . . . 12 (𝑧 = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (π‘₯(leβ€˜πΎ)𝑧 ↔ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
5452, 53imbi12d 345 . . . . . . . . . . 11 (𝑧 = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) ↔ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))))
5554rspcv 3609 . . . . . . . . . 10 (((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡 β†’ (βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))))
5618, 55syl 17 . . . . . . . . 9 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))))
5750, 56mpid 44 . . . . . . . 8 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
5857imp 408 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
5958ad2ant2rl 748 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
60 ralunb 4192 . . . . . . . . 9 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ↔ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯))
61 simpl1 1192 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ 𝐾 ∈ CLat)
62 simpl2 1193 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ 𝑆 βŠ† 𝐡)
63 simpr 486 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ π‘₯ ∈ 𝐡)
641, 2, 3lubl 18465 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯))
6561, 62, 63, 64syl3anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯))
66 simpl3 1194 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ 𝑇 βŠ† 𝐡)
671, 2, 3lubl 18465 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑇 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯ β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯))
6861, 66, 63, 67syl3anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯ β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯))
6965, 68anim12d 610 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯) β†’ ((π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯ ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯)))
7061, 10syl 17 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ 𝐾 ∈ Lat)
7113adantr 482 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
7215adantr 482 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
731, 2, 16latjle12 18403 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ ((π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡 ∧ π‘₯ ∈ 𝐡)) β†’ (((π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯ ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯) ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯))
7470, 71, 72, 63, 73syl13anc 1373 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (((π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯ ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯) ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯))
7569, 74sylibd 238 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯))
7660, 75biimtrid 241 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯))
7776imp 408 . . . . . . 7 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯)
7877adantrr 716 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯)
7918adantr 482 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
801, 2latasymb 18395 . . . . . . . 8 ((𝐾 ∈ Lat ∧ π‘₯ ∈ 𝐡 ∧ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡) β†’ ((π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯) ↔ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
8170, 63, 79, 80syl3anc 1372 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯) ↔ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
8281adantr 482 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) β†’ ((π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯) ↔ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
8359, 78, 82mpbi2and 711 . . . . 5 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) β†’ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
8483ex 414 . . . 4 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) β†’ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
85 elun 4149 . . . . . . . 8 (𝑦 ∈ (𝑆 βˆͺ 𝑇) ↔ (𝑦 ∈ 𝑆 ∨ 𝑦 ∈ 𝑇))
8632, 47jaodan 957 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ (𝑦 ∈ 𝑆 ∨ 𝑦 ∈ 𝑇)) β†’ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
8785, 86sylan2b 595 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ (𝑆 βˆͺ 𝑇)) β†’ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
8887ralrimiva 3147 . . . . . 6 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
89 ralunb 4192 . . . . . . . . 9 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 ↔ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)𝑧))
90 simpl1 1192 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝐾 ∈ CLat)
91 simpl2 1193 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝑆 βŠ† 𝐡)
92 simpr 486 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 ∈ 𝐡)
931, 2, 3lubl 18465 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)𝑧 β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧))
9490, 91, 92, 93syl3anc 1372 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)𝑧 β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧))
95 simpl3 1194 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝑇 βŠ† 𝐡)
961, 2, 3lubl 18465 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑇 βŠ† 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)𝑧 β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧))
9790, 95, 92, 96syl3anc 1372 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)𝑧 β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧))
9894, 97anim12d 610 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)𝑧) β†’ ((π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧 ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧)))
9989, 98biimtrid 241 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧 ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧)))
10090, 10syl 17 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝐾 ∈ Lat)
10190, 91, 12syl2anc 585 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
10290, 95, 14syl2anc 585 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
1031, 2, 16latjle12 18403 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (((π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧 ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧) ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
104100, 101, 102, 92, 103syl13anc 1373 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (((π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧 ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧) ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
10599, 104sylibd 238 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
106105ralrimiva 3147 . . . . . 6 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
107 breq2 5153 . . . . . . . . 9 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (𝑦(leβ€˜πΎ)π‘₯ ↔ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
108107ralbidv 3178 . . . . . . . 8 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ↔ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
109 breq1 5152 . . . . . . . . . 10 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (π‘₯(leβ€˜πΎ)𝑧 ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
110109imbi2d 341 . . . . . . . . 9 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) ↔ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧)))
111110ralbidv 3178 . . . . . . . 8 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) ↔ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧)))
112108, 111anbi12d 632 . . . . . . 7 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) ↔ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))))
113112biimprcd 249 . . . . . 6 ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧)) β†’ (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))))
11488, 106, 113syl2anc 585 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))))
115114adantr 482 . . . 4 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))))
11684, 115impbid 211 . . 3 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) ↔ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
11718, 116riota5 7395 . 2 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (β„©π‘₯ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
1189, 117eqtrd 2773 1 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜(𝑆 βˆͺ 𝑇)) = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062   βˆͺ cun 3947   βŠ† wss 3949   class class class wbr 5149  β€˜cfv 6544  β„©crio 7364  (class class class)co 7409  Basecbs 17144  lecple 17204  lubclub 18262  joincjn 18264  Latclat 18384  CLatccla 18451
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
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  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-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-proset 18248  df-poset 18266  df-lub 18299  df-glb 18300  df-join 18301  df-meet 18302  df-lat 18385  df-clat 18452
This theorem is referenced by:  paddunN  38798  poldmj1N  38799
  Copyright terms: Public domain W3C validator