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

Theorem lubun 17566
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 2797 . . 3 (le‘𝐾) = (le‘𝐾)
3 lubun.u . . 3 𝑈 = (lub‘𝐾)
4 biid 262 . . 3 ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))
5 simp1 1129 . . 3 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → 𝐾 ∈ CLat)
6 unss 4087 . . . . 5 ((𝑆𝐵𝑇𝐵) ↔ (𝑆𝑇) ⊆ 𝐵)
76biimpi 217 . . . 4 ((𝑆𝐵𝑇𝐵) → (𝑆𝑇) ⊆ 𝐵)
873adant1 1123 . . 3 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑆𝑇) ⊆ 𝐵)
91, 2, 3, 4, 5, 8lubval 17427 . 2 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑈‘(𝑆𝑇)) = (𝑥𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
10 clatl 17559 . . . . 5 (𝐾 ∈ CLat → 𝐾 ∈ Lat)
11103ad2ant1 1126 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → 𝐾 ∈ Lat)
121, 3clatlubcl 17555 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑆𝐵) → (𝑈𝑆) ∈ 𝐵)
13123adant3 1125 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑈𝑆) ∈ 𝐵)
141, 3clatlubcl 17555 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑇𝐵) → (𝑈𝑇) ∈ 𝐵)
15143adant2 1124 . . . 4 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑈𝑇) ∈ 𝐵)
16 lubun.j . . . . 5 = (join‘𝐾)
171, 16latjcl 17494 . . . 4 ((𝐾 ∈ Lat ∧ (𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
1811, 13, 15, 17syl3anc 1364 . . 3 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
19 simpl1 1184 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝐾 ∈ CLat)
2019, 10syl 17 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝐾 ∈ Lat)
21 simpl2 1185 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑆𝐵)
22 simpr 485 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑦𝑆)
2321, 22sseldd 3896 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑦𝐵)
2419, 21, 12syl2anc 584 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → (𝑈𝑆) ∈ 𝐵)
25 simpl3 1186 . . . . . . . . . . . . . 14 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑇𝐵)
2619, 25, 14syl2anc 584 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → (𝑈𝑇) ∈ 𝐵)
2720, 24, 26, 17syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
281, 2, 3lubel 17565 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑦𝑆𝑆𝐵) → 𝑦(le‘𝐾)(𝑈𝑆))
2919, 22, 21, 28syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑦(le‘𝐾)(𝑈𝑆))
301, 2, 16latlej1 17503 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵) → (𝑈𝑆)(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
3120, 24, 26, 30syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → (𝑈𝑆)(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
321, 2, 20, 23, 24, 27, 29, 31lattrd 17501 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑆) → 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
3332ralrimiva 3151 . . . . . . . . . 10 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑦𝑆 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
3411adantr 481 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝐾 ∈ Lat)
35 simpl3 1186 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑇𝐵)
36 simpr 485 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑦𝑇)
3735, 36sseldd 3896 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑦𝐵)
38 simpl1 1184 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝐾 ∈ CLat)
3938, 35, 14syl2anc 584 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → (𝑈𝑇) ∈ 𝐵)
4018adantr 481 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
411, 2, 3lubel 17565 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑦𝑇𝑇𝐵) → 𝑦(le‘𝐾)(𝑈𝑇))
4238, 36, 35, 41syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑦(le‘𝐾)(𝑈𝑇))
43 simpl2 1185 . . . . . . . . . . . . . 14 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑆𝐵)
4438, 43, 12syl2anc 584 . . . . . . . . . . . . 13 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → (𝑈𝑆) ∈ 𝐵)
451, 2, 16latlej2 17504 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵) → (𝑈𝑇)(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
4634, 44, 39, 45syl3anc 1364 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → (𝑈𝑇)(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
471, 2, 34, 37, 39, 40, 42, 46lattrd 17501 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦𝑇) → 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
4847ralrimiva 3151 . . . . . . . . . 10 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑦𝑇 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
49 ralunb 4094 . . . . . . . . . 10 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ↔ (∀𝑦𝑆 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ∀𝑦𝑇 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
5033, 48, 49sylanbrc 583 . . . . . . . . 9 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
51 breq2 4972 . . . . . . . . . . . . 13 (𝑧 = ((𝑈𝑆) (𝑈𝑇)) → (𝑦(le‘𝐾)𝑧𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
5251ralbidv 3166 . . . . . . . . . . . 12 (𝑧 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 ↔ ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
53 breq2 4972 . . . . . . . . . . . 12 (𝑧 = ((𝑈𝑆) (𝑈𝑇)) → (𝑥(le‘𝐾)𝑧𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
5452, 53imbi12d 346 . . . . . . . . . . 11 (𝑧 = ((𝑈𝑆) (𝑈𝑇)) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) ↔ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) → 𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))))
5554rspcv 3557 . . . . . . . . . 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 745 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) → 𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
60 ralunb 4094 . . . . . . . . 9 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑥))
61 simpl1 1184 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝐾 ∈ CLat)
62 simpl2 1185 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝑆𝐵)
63 simpr 485 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝑥𝐵)
641, 2, 3lubl 17563 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑥𝐵) → (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 → (𝑈𝑆)(le‘𝐾)𝑥))
6561, 62, 63, 64syl3anc 1364 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 → (𝑈𝑆)(le‘𝐾)𝑥))
66 simpl3 1186 . . . . . . . . . . . 12 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝑇𝐵)
671, 2, 3lubl 17563 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑇𝐵𝑥𝐵) → (∀𝑦𝑇 𝑦(le‘𝐾)𝑥 → (𝑈𝑇)(le‘𝐾)𝑥))
6861, 66, 63, 67syl3anc 1364 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (∀𝑦𝑇 𝑦(le‘𝐾)𝑥 → (𝑈𝑇)(le‘𝐾)𝑥))
6965, 68anim12d 608 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑥) → ((𝑈𝑆)(le‘𝐾)𝑥 ∧ (𝑈𝑇)(le‘𝐾)𝑥)))
7061, 10syl 17 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → 𝐾 ∈ Lat)
7113adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (𝑈𝑆) ∈ 𝐵)
7215adantr 481 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (𝑈𝑇) ∈ 𝐵)
731, 2, 16latjle12 17505 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ ((𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵𝑥𝐵)) → (((𝑈𝑆)(le‘𝐾)𝑥 ∧ (𝑈𝑇)(le‘𝐾)𝑥) ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥))
7470, 71, 72, 63, 73syl13anc 1365 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (((𝑈𝑆)(le‘𝐾)𝑥 ∧ (𝑈𝑇)(le‘𝐾)𝑥) ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥))
7569, 74sylibd 240 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑥) → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥))
7660, 75syl5bi 243 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥))
7776imp 407 . . . . . . 7 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥) → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥)
7877adantrr 713 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥)
7918adantr 481 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵)
801, 2latasymb 17497 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑥𝐵 ∧ ((𝑈𝑆) (𝑈𝑇)) ∈ 𝐵) → ((𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥) ↔ 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
8170, 63, 79, 80syl3anc 1364 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥) ↔ 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
8281adantr 481 . . . . . 6 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) → ((𝑥(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑥) ↔ 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
8359, 78, 82mpbi2and 708 . . . . 5 ((((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) ∧ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) → 𝑥 = ((𝑈𝑆) (𝑈𝑇)))
8483ex 413 . . . 4 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) → 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
85 elun 4052 . . . . . . . 8 (𝑦 ∈ (𝑆𝑇) ↔ (𝑦𝑆𝑦𝑇))
8632, 47jaodan 952 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ (𝑦𝑆𝑦𝑇)) → 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
8785, 86sylan2b 593 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑦 ∈ (𝑆𝑇)) → 𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
8887ralrimiva 3151 . . . . . 6 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)))
89 ralunb 4094 . . . . . . . . 9 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑧 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑧))
90 simpl1 1184 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ CLat)
91 simpl2 1185 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝑆𝐵)
92 simpr 485 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝑧𝐵)
931, 2, 3lubl 17563 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑧𝐵) → (∀𝑦𝑆 𝑦(le‘𝐾)𝑧 → (𝑈𝑆)(le‘𝐾)𝑧))
9490, 91, 92, 93syl3anc 1364 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (∀𝑦𝑆 𝑦(le‘𝐾)𝑧 → (𝑈𝑆)(le‘𝐾)𝑧))
95 simpl3 1186 . . . . . . . . . . 11 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → 𝑇𝐵)
961, 2, 3lubl 17563 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑇𝐵𝑧𝐵) → (∀𝑦𝑇 𝑦(le‘𝐾)𝑧 → (𝑈𝑇)(le‘𝐾)𝑧))
9790, 95, 92, 96syl3anc 1364 . . . . . . . . . 10 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (∀𝑦𝑇 𝑦(le‘𝐾)𝑧 → (𝑈𝑇)(le‘𝐾)𝑧))
9894, 97anim12d 608 . . . . . . . . 9 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → ((∀𝑦𝑆 𝑦(le‘𝐾)𝑧 ∧ ∀𝑦𝑇 𝑦(le‘𝐾)𝑧) → ((𝑈𝑆)(le‘𝐾)𝑧 ∧ (𝑈𝑇)(le‘𝐾)𝑧)))
9989, 98syl5bi 243 . . . . . . . 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 17505 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑈𝑆) ∈ 𝐵 ∧ (𝑈𝑇) ∈ 𝐵𝑧𝐵)) → (((𝑈𝑆)(le‘𝐾)𝑧 ∧ (𝑈𝑇)(le‘𝐾)𝑧) ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
104100, 101, 102, 92, 103syl13anc 1365 . . . . . . . 8 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (((𝑈𝑆)(le‘𝐾)𝑧 ∧ (𝑈𝑇)(le‘𝐾)𝑧) ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
10599, 104sylibd 240 . . . . . . 7 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑧𝐵) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
106105ralrimiva 3151 . . . . . 6 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
107 breq2 4972 . . . . . . . . 9 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (𝑦(le‘𝐾)𝑥𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
108107ralbidv 3166 . . . . . . . 8 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ↔ ∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇))))
109 breq1 4971 . . . . . . . . . 10 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (𝑥(le‘𝐾)𝑧 ↔ ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))
110109imbi2d 342 . . . . . . . . 9 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) ↔ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧)))
111110ralbidv 3166 . . . . . . . 8 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → (∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧) ↔ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧)))
112108, 111anbi12d 630 . . . . . . 7 (𝑥 = ((𝑈𝑆) (𝑈𝑇)) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)((𝑈𝑆) (𝑈𝑇)) ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧 → ((𝑈𝑆) (𝑈𝑇))(le‘𝐾)𝑧))))
113112biimprcd 251 . . . . . 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 213 . . 3 (((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) ∧ 𝑥𝐵) → ((∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) ↔ 𝑥 = ((𝑈𝑆) (𝑈𝑇))))
11718, 116riota5 7010 . 2 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑥𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑥 ∧ ∀𝑧𝐵 (∀𝑦 ∈ (𝑆𝑇)𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) = ((𝑈𝑆) (𝑈𝑇)))
1189, 117eqtrd 2833 1 ((𝐾 ∈ CLat ∧ 𝑆𝐵𝑇𝐵) → (𝑈‘(𝑆𝑇)) = ((𝑈𝑆) (𝑈𝑇)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 842  w3a 1080   = wceq 1525  wcel 2083  wral 3107  cun 3863  wss 3865   class class class wbr 4968  cfv 6232  crio 6983  (class class class)co 7023  Basecbs 16316  lecple 16405  lubclub 17385  joincjn 17387  Latclat 17488  CLatccla 17550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-proset 17371  df-poset 17389  df-lub 17417  df-glb 17418  df-join 17419  df-meet 17420  df-lat 17489  df-clat 17551
This theorem is referenced by:  paddunN  36615  poldmj1N  36616
  Copyright terms: Public domain W3C validator