This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lubun

Description: The LUB of a union. (Contributed by NM, 5-Mar-2012)

Ref Expression
Hypotheses lubun.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lubun.j ⊢ ∨ = ( join ‘ 𝐾 )
lubun.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
Assertion lubun ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑈 ‘ ( 𝑆 ∪ 𝑇 ) ) = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 lubun.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lubun.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lubun.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 biid ⊢ ( ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
6 simp1 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → 𝐾 ∈ CLat )
7 unss ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ↔ ( 𝑆 ∪ 𝑇 ) ⊆ 𝐵 )
8 7 biimpi ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑆 ∪ 𝑇 ) ⊆ 𝐵 )
9 8 3adant1 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑆 ∪ 𝑇 ) ⊆ 𝐵 )
10 1 4 3 5 6 9 lubval ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑈 ‘ ( 𝑆 ∪ 𝑇 ) ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
11 clatl ⊢ ( 𝐾 ∈ CLat → 𝐾 ∈ Lat )
12 11 3ad2ant1 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → 𝐾 ∈ Lat )
13 1 3 clatlubcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
14 13 3adant3 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
15 1 3 clatlubcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 )
16 15 3adant2 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 )
17 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∈ 𝐵 )
18 12 14 16 17 syl3anc ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∈ 𝐵 )
19 simpl1 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐾 ∈ CLat )
20 19 11 syl ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐾 ∈ Lat )
21 simpl2 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
22 simpr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
23 21 22 sseldd ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝐵 )
24 19 21 13 syl2anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
25 simpl3 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑇 ⊆ 𝐵 )
26 19 25 15 syl2anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 )
27 20 24 26 17 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∈ 𝐵 )
28 1 4 3 lubel ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑦 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑈 ‘ 𝑆 ) )
29 19 22 21 28 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑈 ‘ 𝑆 ) )
30 1 4 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 ) → ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
31 20 24 26 30 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
32 1 4 20 23 24 27 29 31 lattrd ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
33 32 ralrimiva ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
34 12 adantr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → 𝐾 ∈ Lat )
35 simpl3 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑇 ⊆ 𝐵 )
36 simpr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ 𝑇 )
37 35 36 sseldd ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ 𝐵 )
38 simpl1 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → 𝐾 ∈ CLat )
39 38 35 15 syl2anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 )
40 18 adantr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∈ 𝐵 )
41 1 4 3 lubel ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑦 ∈ 𝑇 ∧ 𝑇 ⊆ 𝐵 ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑈 ‘ 𝑇 ) )
42 38 36 35 41 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑈 ‘ 𝑇 ) )
43 simpl2 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑆 ⊆ 𝐵 )
44 38 43 13 syl2anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
45 1 4 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 ) → ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
46 34 44 39 45 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
47 1 4 34 37 39 40 42 46 lattrd ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
48 47 ralrimiva ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
49 ralunb ⊢ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∧ ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
50 33 48 49 sylanbrc ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
51 breq2 ⊢ ( 𝑧 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( 𝑦 ( le ‘ 𝐾 ) 𝑧 ↔ 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
52 51 ralbidv ⊢ ( 𝑧 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
53 breq2 ⊢ ( 𝑧 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑧 ↔ 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
54 52 53 imbi12d ⊢ ( 𝑧 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) ) )
55 54 rspcv ⊢ ( ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∈ 𝐵 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) ) )
56 18 55 syl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) ) )
57 50 56 mpid ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
58 57 imp ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
59 58 ad2ant2rl ⊢ ( ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) → 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
60 ralunb ⊢ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
61 simpl1 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐾 ∈ CLat )
62 simpl2 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ⊆ 𝐵 )
63 simpr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
64 1 4 3 lubl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 → ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 ) )
65 61 62 63 64 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 → ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 ) )
66 simpl3 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑇 ⊆ 𝐵 )
67 1 4 3 lubl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑥 → ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑥 ) )
68 61 66 63 67 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑥 → ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑥 ) )
69 65 68 anim12d ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → ( ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 ∧ ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑥 ) ) )
70 61 11 syl ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐾 ∈ Lat )
71 14 adantr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
72 16 adantr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 )
73 1 4 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 ∧ ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑥 ) ↔ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 ) )
74 70 71 72 63 73 syl13anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑥 ∧ ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑥 ) ↔ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 ) )
75 69 74 sylibd ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 ) )
76 60 75 biimtrid ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 ) )
77 76 imp ⊢ ( ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 )
78 77 adantrr ⊢ ( ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 )
79 18 adantr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∈ 𝐵 )
80 1 4 latasymb ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∈ 𝐵 ) → ( ( 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∧ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 ) ↔ 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
81 70 63 79 80 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∧ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 ) ↔ 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
82 81 adantr ⊢ ( ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) → ( ( 𝑥 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∧ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑥 ) ↔ 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
83 59 78 82 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) → 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
84 83 ex ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) → 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
85 elun ⊢ ( 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) ↔ ( 𝑦 ∈ 𝑆 ∨ 𝑦 ∈ 𝑇 ) )
86 32 47 jaodan ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑆 ∨ 𝑦 ∈ 𝑇 ) ) → 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
87 85 86 sylan2b ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) ) → 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
88 87 ralrimiva ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
89 ralunb ⊢ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑧 ) )
90 simpl1 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ CLat )
91 simpl2 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑆 ⊆ 𝐵 )
92 simpr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
93 1 4 3 lubl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑧 ) )
94 90 91 92 93 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑧 ) )
95 simpl3 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑇 ⊆ 𝐵 )
96 1 4 3 lubl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑧 ) )
97 90 95 92 96 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑧 ) )
98 94 97 anim12d ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → ( ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑧 ∧ ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑧 ) ) )
99 89 98 biimtrid ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑧 ∧ ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑧 ) ) )
100 90 11 syl ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ Lat )
101 90 91 13 syl2anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
102 90 95 15 syl2anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 )
103 1 4 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑧 ∧ ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) )
104 100 101 102 92 103 syl13anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑈 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑧 ∧ ( 𝑈 ‘ 𝑇 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) )
105 99 104 sylibd ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) )
106 105 ralrimiva ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) )
107 breq2 ⊢ ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( 𝑦 ( le ‘ 𝐾 ) 𝑥 ↔ 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
108 107 ralbidv ⊢ ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ↔ ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
109 breq1 ⊢ ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑧 ↔ ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) )
110 109 imbi2d ⊢ ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) ) )
111 110 ralbidv ⊢ ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) ) )
112 108 111 anbi12d ⊢ ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) ) ) )
113 112 biimprcd ⊢ ( ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ( le ‘ 𝐾 ) 𝑧 ) ) → ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
114 88 106 113 syl2anc ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
115 114 adantr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) → ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
116 84 115 impbid ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ 𝑥 = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) ) )
117 18 116 riota5 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ ( 𝑆 ∪ 𝑇 ) 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )
118 10 117 eqtrd ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑈 ‘ ( 𝑆 ∪ 𝑇 ) ) = ( ( 𝑈 ‘ 𝑆 ) ∨ ( 𝑈 ‘ 𝑇 ) ) )