MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lubun Structured version   Visualization version   GIF version

Theorem lubun 18542
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 2726 . . 3 (le‘𝐾) = (le‘𝐾)
3 lubun.u . . 3 𝑈 = (lub‘𝐾)
4 biid 260 . . 3 ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))
5 simp1 1133 . . 3 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → 𝐾 ∈ CLat)
6 unss 4185 . . . . 5 ((𝑆𝐵𝑇𝐵) ↔ (𝑆𝑇) ⊆ 𝐵)
76biimpi 215 . . . 4 ((𝑆𝐵𝑇𝐵) → (𝑆𝑇) ⊆ 𝐵)
873adant1 1127 . . 3 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑆𝑇) ⊆ 𝐵)
91, 2, 3, 4, 5, 8lubval 18383 . 2 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑈‘(𝑆𝑇)) = (𝑥𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
10 clatl 18535 . . . . 5 (𝐾 ∈ CLat → 𝐾 ∈ Lat)
11103ad2ant1 1130 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → 𝐾 ∈ Lat)
121, 3clatlubcl 18530 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑆𝐵) → (𝑈𝑆) ∈ 𝐵)
13123adant3 1129 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑈𝑆) ∈ 𝐵)
141, 3clatlubcl 18530 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑇𝐵) → (𝑈𝑇) ∈ 𝐵)
15143adant2 1128 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑈𝑇) ∈ 𝐵)
16 lubun.j . . . . 5 = (join‘𝐾)
171, 16latjcl 18466 . . . 4 ((𝐾 ∈ Lat ∧ (𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
1811, 13, 15, 17syl3anc 1368 . . 3 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
19 simpl1 1188 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝐾 ∈ CLat)
2019, 10syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝐾 ∈ Lat)
21 simpl2 1189 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑆𝐵)
22 simpr 483 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑦𝑆)
2321, 22sseldd 3980 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑦𝐵)
2419, 21, 12syl2anc 582 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → (𝑈𝑆) ∈ 𝐵)
25 simpl3 1190 . . . . . . . . . . . . . 14 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑇𝐵)
2619, 25, 14syl2anc 582 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → (𝑈𝑇) ∈ 𝐵)
2720, 24, 26, 17syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
281, 2, 3lubel 18541 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑦𝑆𝑆𝐵) → 𝑦(le‘𝐾)(𝑈𝑆))
2919, 22, 21, 28syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑦(le‘𝐾)(𝑈𝑆))
301, 2, 16latlej1 18475 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵) → (𝑈𝑆)(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
3120, 24, 26, 30syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → (𝑈𝑆)(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
321, 2, 20, 23, 24, 27, 29, 31lattrd 18473 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
3332ralrimiva 3136 . . . . . . . . . 10 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑦𝑆 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
3411adantr 479 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝐾 ∈ Lat)
35 simpl3 1190 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑇𝐵)
36 simpr 483 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑦𝑇)
3735, 36sseldd 3980 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑦𝐵)
38 simpl1 1188 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝐾 ∈ CLat)
3938, 35, 14syl2anc 582 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → (𝑈𝑇) ∈ 𝐵)
4018adantr 479 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
411, 2, 3lubel 18541 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑦𝑇𝑇𝐵) → 𝑦(le‘𝐾)(𝑈𝑇))
4238, 36, 35, 41syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑦(le‘𝐾)(𝑈𝑇))
43 simpl2 1189 . . . . . . . . . . . . . 14 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑆𝐵)
4438, 43, 12syl2anc 582 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → (𝑈𝑆) ∈ 𝐵)
451, 2, 16latlej2 18476 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵) → (𝑈𝑇)(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
4634, 44, 39, 45syl3anc 1368 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → (𝑈𝑇)(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
471, 2, 34, 37, 39, 40, 42, 46lattrd 18473 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
4847ralrimiva 3136 . . . . . . . . . 10 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑦𝑇 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
49 ralunb 4192 . . . . . . . . . 10 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ↔ (∀𝑦𝑆 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ∀𝑦𝑇 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
5033, 48, 49sylanbrc 581 . . . . . . . . 9 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
51 breq2 5159 . . . . . . . . . . . . 13 (𝑧 = ((𝑈𝑆) (𝑈𝑇)) → (𝑦(le‘𝐾)𝑧𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
5251ralbidv 3168 . . . . . . . . . . . 12 (𝑧 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 ↔ ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
53 breq2 5159 . . . . . . . . . . . 12 (𝑧 = ((𝑈𝑆) (𝑈𝑇)) → (𝑥(le‘𝐾)𝑧𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
5452, 53imbi12d 343 . . . . . . . . . . 11 (𝑧 = ((𝑈𝑆) (𝑈𝑇)) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) ↔ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) → 𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))))
5554rspcv 3604 . . . . . . . . . 10 (((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵 → (∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) → 𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))))
5618, 55syl 17 . . . . . . . . 9 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) → 𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))))
5750, 56mpid 44 . . . . . . . 8 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) → 𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
5857imp 405 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) → 𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
5958ad2ant2rl 747 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) → 𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
60 ralunb 4192 . . . . . . . . 9 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑥))
61 simpl1 1188 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝐾 ∈ CLat)
62 simpl2 1189 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝑆𝐵)
63 simpr 483 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝑥𝐵)
641, 2, 3lubl 18539 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑥𝐵) → (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 → (𝑈𝑆)(le‘𝐾)𝑥))
6561, 62, 63, 64syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 → (𝑈𝑆)(le‘𝐾)𝑥))
66 simpl3 1190 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝑇𝐵)
671, 2, 3lubl 18539 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑇𝐵𝑥𝐵) → (∀𝑦𝑇 𝑦(le‘𝐾)𝑥 → (𝑈𝑇)(le‘𝐾)𝑥))
6861, 66, 63, 67syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (∀𝑦𝑇 𝑦(le‘𝐾)𝑥 → (𝑈𝑇)(le‘𝐾)𝑥))
6965, 68anim12d 607 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑥) → ((𝑈𝑆)(le‘𝐾)𝑥 ∧ (𝑈𝑇)(le‘𝐾)𝑥)))
7061, 10syl 17 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝐾 ∈ Lat)
7113adantr 479 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (𝑈𝑆) ∈ 𝐵)
7215adantr 479 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (𝑈𝑇) ∈ 𝐵)
731, 2, 16latjle12 18477 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ ((𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵𝑥𝐵)) → (((𝑈𝑆)(le‘𝐾)𝑥 ∧ (𝑈𝑇)(le‘𝐾)𝑥) ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥))
7470, 71, 72, 63, 73syl13anc 1369 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (((𝑈𝑆)(le‘𝐾)𝑥 ∧ (𝑈𝑇)(le‘𝐾)𝑥) ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥))
7569, 74sylibd 238 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑥) → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥))
7660, 75biimtrid 241 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥))
7776imp 405 . . . . . . 7 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥) → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥)
7877adantrr 715 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥)
7918adantr 479 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
801, 2latasymb 18469 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑥𝐵 ∧ ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵) → ((𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥) ↔ 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
8170, 63, 79, 80syl3anc 1368 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥) ↔ 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
8281adantr 479 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) → ((𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥) ↔ 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
8359, 78, 82mpbi2and 710 . . . . 5 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) → 𝑥 = ((𝑈𝑆) (𝑈𝑇)))
8483ex 411 . . . 4 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) → 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
85 elun 4148 . . . . . . . 8 (𝑦 ∈ (𝑆𝑇) ↔ (𝑦𝑆𝑦𝑇))
8632, 47jaodan 955 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ (𝑦𝑆𝑦𝑇)) → 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
8785, 86sylan2b 592 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦 ∈ (𝑆𝑇)) → 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
8887ralrimiva 3136 . . . . . 6 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
89 ralunb 4192 . . . . . . . . 9 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑧 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑧))
90 simpl1 1188 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ CLat)
91 simpl2 1189 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝑆𝐵)
92 simpr 483 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝑧𝐵)
931, 2, 3lubl 18539 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑧𝐵) → (∀𝑦𝑆 𝑦(le‘𝐾)𝑧 → (𝑈𝑆)(le‘𝐾)𝑧))
9490, 91, 92, 93syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (∀𝑦𝑆 𝑦(le‘𝐾)𝑧 → (𝑈𝑆)(le‘𝐾)𝑧))
95 simpl3 1190 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝑇𝐵)
961, 2, 3lubl 18539 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑇𝐵𝑧𝐵) → (∀𝑦𝑇 𝑦(le‘𝐾)𝑧 → (𝑈𝑇)(le‘𝐾)𝑧))
9790, 95, 92, 96syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (∀𝑦𝑇 𝑦(le‘𝐾)𝑧 → (𝑈𝑇)(le‘𝐾)𝑧))
9894, 97anim12d 607 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → ((∀𝑦𝑆 𝑦(le‘𝐾)𝑧 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑧) → ((𝑈𝑆)(le‘𝐾)𝑧 ∧ (𝑈𝑇)(le‘𝐾)𝑧)))
9989, 98biimtrid 241 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆)(le‘𝐾)𝑧 ∧ (𝑈𝑇)(le‘𝐾)𝑧)))
10090, 10syl 17 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ Lat)
10190, 91, 12syl2anc 582 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (𝑈𝑆) ∈ 𝐵)
10290, 95, 14syl2anc 582 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (𝑈𝑇) ∈ 𝐵)
1031, 2, 16latjle12 18477 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵𝑧𝐵)) → (((𝑈𝑆)(le‘𝐾)𝑧 ∧ (𝑈𝑇)(le‘𝐾)𝑧) ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
104100, 101, 102, 92, 103syl13anc 1369 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (((𝑈𝑆)(le‘𝐾)𝑧 ∧ (𝑈𝑇)(le‘𝐾)𝑧) ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
10599, 104sylibd 238 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
106105ralrimiva 3136 . . . . . 6 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
107 breq2 5159 . . . . . . . . 9 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (𝑦(le‘𝐾)𝑥𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
108107ralbidv 3168 . . . . . . . 8 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ↔ ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
109 breq1 5158 . . . . . . . . . 10 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (𝑥(le‘𝐾)𝑧 ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
110109imbi2d 339 . . . . . . . . 9 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) ↔ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧)))
111110ralbidv 3168 . . . . . . . 8 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) ↔ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧)))
112108, 111anbi12d 630 . . . . . . 7 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))))
113112biimprcd 249 . . . . . 6 ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧)) → (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
11488, 106, 113syl2anc 582 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
115114adantr 479 . . . 4 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
11684, 115impbid 211 . . 3 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) ↔ 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
11718, 116riota5 7412 . 2 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑥𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) = ((𝑈𝑆) (𝑈𝑇)))
1189, 117eqtrd 2766 1 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑈‘(𝑆𝑇)) = ((𝑈𝑆) (𝑈𝑇)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 845  w3a 1084   = wceq 1534  wcel 2099  wral 3051  cun 3945  wss 3947   class class class wbr 5155  cfv 6556  crio 7381  (class class class)co 7426  Basecbs 17215  lecple 17275  lubclub 18336  joincjn 18338  Latclat 18458  CLatccla 18525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5292  ax-sep 5306  ax-nul 5313  ax-pow 5371  ax-pr 5435  ax-un 7748
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-iun 5005  df-br 5156  df-opab 5218  df-mpt 5239  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-riota 7382  df-ov 7429  df-oprab 7430  df-proset 18322  df-poset 18340  df-lub 18373  df-glb 18374  df-join 18375  df-meet 18376  df-lat 18459  df-clat 18526
This theorem is referenced by:  paddunN  39628  poldmj1N  39629
  Copyright terms: Public domain W3C validator