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