Metamath Proof Explorer

Theorem lubun

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

Ref Expression
Hypotheses lubun.b ⊢ B = Base K
lubun.j ⊢ ∨ ˙ = join ⁡ K
lubun.u ⊢ U = lub ⁡ K
Assertion lubun ⊢ K ∈ CLat ∧ S ⊆ B ∧ T ⊆ B → U ⁡ S ∪ T = U ⁡ S ∨ ˙ U ⁡ T

Proof

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