MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lubun Structured version   Visualization version   GIF version
Theorem lubun 18433
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 2731 . . 3 (leβ€˜πΎ) = (leβ€˜πΎ)
3 lubun.u . . 3 π‘ˆ = (lubβ€˜πΎ)
4 biid 260 . . 3 ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) ↔ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)))
5 simp1 1136 . . 3 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ 𝐾 ∈ CLat)
6 unss 4164 . . . . 5 ((𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ↔ (𝑆 βˆͺ 𝑇) βŠ† 𝐡)
76biimpi 215 . . . 4 ((𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (𝑆 βˆͺ 𝑇) βŠ† 𝐡)
873adant1 1130 . . 3 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (𝑆 βˆͺ 𝑇) βŠ† 𝐡)
91, 2, 3, 4, 5, 8lubval 18274 . 2 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜(𝑆 βˆͺ 𝑇)) = (β„©π‘₯ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))))
10 clatl 18426 . . . . 5 (𝐾 ∈ CLat β†’ 𝐾 ∈ Lat)
11103ad2ant1 1133 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ 𝐾 ∈ Lat)
121, 3clatlubcl 18421 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
13123adant3 1132 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
141, 3clatlubcl 18421 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
15143adant2 1131 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
16 lubun.j . . . . 5 ∨ = (joinβ€˜πΎ)
171, 16latjcl 18357 . . . 4 ((𝐾 ∈ Lat ∧ (π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
1811, 13, 15, 17syl3anc 1371 . . 3 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
19 simpl1 1191 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝐾 ∈ CLat)
2019, 10syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝐾 ∈ Lat)
21 simpl2 1192 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑆 βŠ† 𝐡)
22 simpr 485 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 ∈ 𝑆)
2321, 22sseldd 3963 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 ∈ 𝐡)
2419, 21, 12syl2anc 584 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
25 simpl3 1193 . . . . . . . . . . . . . 14 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑇 βŠ† 𝐡)
2619, 25, 14syl2anc 584 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
2720, 24, 26, 17syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
281, 2, 3lubel 18432 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑦 ∈ 𝑆 ∧ 𝑆 βŠ† 𝐡) β†’ 𝑦(leβ€˜πΎ)(π‘ˆβ€˜π‘†))
2919, 22, 21, 28syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦(leβ€˜πΎ)(π‘ˆβ€˜π‘†))
301, 2, 16latlej1 18366 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡) β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
3120, 24, 26, 30syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
321, 2, 20, 23, 24, 27, 29, 31lattrd 18364 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
3332ralrimiva 3145 . . . . . . . . . 10 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
3411adantr 481 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝐾 ∈ Lat)
35 simpl3 1193 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑇 βŠ† 𝐡)
36 simpr 485 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑦 ∈ 𝑇)
3735, 36sseldd 3963 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑦 ∈ 𝐡)
38 simpl1 1191 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝐾 ∈ CLat)
3938, 35, 14syl2anc 584 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
4018adantr 481 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
411, 2, 3lubel 18432 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑦 ∈ 𝑇 ∧ 𝑇 βŠ† 𝐡) β†’ 𝑦(leβ€˜πΎ)(π‘ˆβ€˜π‘‡))
4238, 36, 35, 41syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑦(leβ€˜πΎ)(π‘ˆβ€˜π‘‡))
43 simpl2 1192 . . . . . . . . . . . . . 14 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑆 βŠ† 𝐡)
4438, 43, 12syl2anc 584 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
451, 2, 16latlej2 18367 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡) β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
4634, 44, 39, 45syl3anc 1371 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
471, 2, 34, 37, 39, 40, 42, 46lattrd 18364 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ 𝑇) β†’ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
4847ralrimiva 3145 . . . . . . . . . 10 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
49 ralunb 4171 . . . . . . . . . 10 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ↔ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
5033, 48, 49sylanbrc 583 . . . . . . . . 9 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
51 breq2 5129 . . . . . . . . . . . . 13 (𝑧 = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (𝑦(leβ€˜πΎ)𝑧 ↔ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
5251ralbidv 3176 . . . . . . . . . . . 12 (𝑧 = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 ↔ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
53 breq2 5129 . . . . . . . . . . . 12 (𝑧 = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (π‘₯(leβ€˜πΎ)𝑧 ↔ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
5452, 53imbi12d 344 . . . . . . . . . . 11 (𝑧 = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) ↔ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))))
5554rspcv 3591 . . . . . . . . . 10 (((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡 β†’ (βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))))
5618, 55syl 17 . . . . . . . . 9 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))))
5750, 56mpid 44 . . . . . . . 8 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
5857imp 407 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
5958ad2ant2rl 747 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) β†’ π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
60 ralunb 4171 . . . . . . . . 9 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ↔ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯))
61 simpl1 1191 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ 𝐾 ∈ CLat)
62 simpl2 1192 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ 𝑆 βŠ† 𝐡)
63 simpr 485 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ π‘₯ ∈ 𝐡)
641, 2, 3lubl 18430 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯))
6561, 62, 63, 64syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯))
66 simpl3 1193 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ 𝑇 βŠ† 𝐡)
671, 2, 3lubl 18430 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑇 βŠ† 𝐡 ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯ β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯))
6861, 66, 63, 67syl3anc 1371 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯ β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯))
6965, 68anim12d 609 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯) β†’ ((π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯ ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯)))
7061, 10syl 17 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ 𝐾 ∈ Lat)
7113adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
7215adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
731, 2, 16latjle12 18368 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ ((π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡 ∧ π‘₯ ∈ 𝐡)) β†’ (((π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯ ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯) ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯))
7470, 71, 72, 63, 73syl13anc 1372 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (((π‘ˆβ€˜π‘†)(leβ€˜πΎ)π‘₯ ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)π‘₯) ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯))
7569, 74sylibd 238 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)π‘₯) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯))
7660, 75biimtrid 241 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯))
7776imp 407 . . . . . . 7 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯)
7877adantrr 715 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯)
7918adantr 481 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡)
801, 2latasymb 18360 . . . . . . . 8 ((𝐾 ∈ Lat ∧ π‘₯ ∈ 𝐡 ∧ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∈ 𝐡) β†’ ((π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯) ↔ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
8170, 63, 79, 80syl3anc 1371 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯) ↔ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
8281adantr 481 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) β†’ ((π‘₯(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)π‘₯) ↔ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
8359, 78, 82mpbi2and 710 . . . . 5 ((((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) ∧ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) β†’ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
8483ex 413 . . . 4 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) β†’ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
85 elun 4128 . . . . . . . 8 (𝑦 ∈ (𝑆 βˆͺ 𝑇) ↔ (𝑦 ∈ 𝑆 ∨ 𝑦 ∈ 𝑇))
8632, 47jaodan 956 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ (𝑦 ∈ 𝑆 ∨ 𝑦 ∈ 𝑇)) β†’ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
8785, 86sylan2b 594 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑦 ∈ (𝑆 βˆͺ 𝑇)) β†’ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
8887ralrimiva 3145 . . . . . 6 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
89 ralunb 4171 . . . . . . . . 9 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 ↔ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)𝑧))
90 simpl1 1191 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝐾 ∈ CLat)
91 simpl2 1192 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝑆 βŠ† 𝐡)
92 simpr 485 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 ∈ 𝐡)
931, 2, 3lubl 18430 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)𝑧 β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧))
9490, 91, 92, 93syl3anc 1371 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)𝑧 β†’ (π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧))
95 simpl3 1193 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝑇 βŠ† 𝐡)
961, 2, 3lubl 18430 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑇 βŠ† 𝐡 ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)𝑧 β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧))
9790, 95, 92, 96syl3anc 1371 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)𝑧 β†’ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧))
9894, 97anim12d 609 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ 𝑆 𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘¦ ∈ 𝑇 𝑦(leβ€˜πΎ)𝑧) β†’ ((π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧 ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧)))
9989, 98biimtrid 241 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧 ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧)))
10090, 10syl 17 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝐾 ∈ Lat)
10190, 91, 12syl2anc 584 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (π‘ˆβ€˜π‘†) ∈ 𝐡)
10290, 95, 14syl2anc 584 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (π‘ˆβ€˜π‘‡) ∈ 𝐡)
1031, 2, 16latjle12 18368 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((π‘ˆβ€˜π‘†) ∈ 𝐡 ∧ (π‘ˆβ€˜π‘‡) ∈ 𝐡 ∧ 𝑧 ∈ 𝐡)) β†’ (((π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧 ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧) ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
104100, 101, 102, 92, 103syl13anc 1372 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (((π‘ˆβ€˜π‘†)(leβ€˜πΎ)𝑧 ∧ (π‘ˆβ€˜π‘‡)(leβ€˜πΎ)𝑧) ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
10599, 104sylibd 238 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
106105ralrimiva 3145 . . . . . 6 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
107 breq2 5129 . . . . . . . . 9 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (𝑦(leβ€˜πΎ)π‘₯ ↔ 𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
108107ralbidv 3176 . . . . . . . 8 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ↔ βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
109 breq1 5128 . . . . . . . . . 10 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (π‘₯(leβ€˜πΎ)𝑧 ↔ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))
110109imbi2d 340 . . . . . . . . 9 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) ↔ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧)))
111110ralbidv 3176 . . . . . . . 8 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧) ↔ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧)))
112108, 111anbi12d 631 . . . . . . 7 (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) ↔ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧))))
113112biimprcd 249 . . . . . 6 ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))(leβ€˜πΎ)𝑧)) β†’ (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))))
11488, 106, 113syl2anc 584 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))))
115114adantr 481 . . . 4 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)) β†’ (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))))
11684, 115impbid 211 . . 3 (((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) ∧ π‘₯ ∈ 𝐡) β†’ ((βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧)) ↔ π‘₯ = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡))))
11718, 116riota5 7363 . 2 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (β„©π‘₯ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)π‘₯ ∧ βˆ€π‘§ ∈ 𝐡 (βˆ€π‘¦ ∈ (𝑆 βˆͺ 𝑇)𝑦(leβ€˜πΎ)𝑧 β†’ π‘₯(leβ€˜πΎ)𝑧))) = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
1189, 117eqtrd 2771 1 ((𝐾 ∈ CLat ∧ 𝑆 βŠ† 𝐡 ∧ 𝑇 βŠ† 𝐡) β†’ (π‘ˆβ€˜(𝑆 βˆͺ 𝑇)) = ((π‘ˆβ€˜π‘†) ∨ (π‘ˆβ€˜π‘‡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3060   βˆͺ cun 3926   βŠ† wss 3928   class class class wbr 5125  β€˜cfv 6516  β„©crio 7332  (class class class)co 7377  Basecbs 17109  lecple 17169  lubclub 18227  joincjn 18229  Latclat 18349  CLatccla 18416
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 2702  ax-rep 5262  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-iun 4976  df-br 5126  df-opab 5188  df-mpt 5209  df-id 5551  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7333  df-ov 7380  df-oprab 7381  df-proset 18213  df-poset 18231  df-lub 18264  df-glb 18265  df-join 18266  df-meet 18267  df-lat 18350  df-clat 18417
This theorem is referenced by:  paddunN  38496  poldmj1N  38497
  Copyright terms: Public domain W3C validator