Step |
Hyp |
Ref |
Expression |
1 |
|
glbcon.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
glbcon.u |
⊢ 𝑈 = ( lub ‘ 𝐾 ) |
3 |
|
glbcon.g |
⊢ 𝐺 = ( glb ‘ 𝐾 ) |
4 |
|
glbcon.o |
⊢ ⊥ = ( oc ‘ 𝐾 ) |
5 |
|
vex |
⊢ 𝑦 ∈ V |
6 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑆 ↔ 𝑦 = 𝑆 ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ) ) |
8 |
5 7
|
elab |
⊢ ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ) |
9 |
|
nfra1 |
⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 |
10 |
|
nfv |
⊢ Ⅎ 𝑖 𝑦 ∈ 𝐵 |
11 |
|
rsp |
⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑖 ∈ 𝐼 → 𝑆 ∈ 𝐵 ) ) |
12 |
|
eleq1a |
⊢ ( 𝑆 ∈ 𝐵 → ( 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) ) |
13 |
11 12
|
syl6 |
⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑖 ∈ 𝐼 → ( 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) ) ) |
14 |
9 10 13
|
rexlimd |
⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) ) |
15 |
8 14
|
syl5bi |
⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } → 𝑦 ∈ 𝐵 ) ) |
16 |
15
|
ssrdv |
⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ⊆ 𝐵 ) |
17 |
1 2 3 4
|
glbconN |
⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ⊆ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) ) |
18 |
16 17
|
sylan2 |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) ) |
19 |
|
fvex |
⊢ ( ⊥ ‘ 𝑦 ) ∈ V |
20 |
|
eqeq1 |
⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑥 = 𝑆 ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) |
21 |
20
|
rexbidv |
⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 ↔ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) |
22 |
19 21
|
elab |
⊢ ( ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ↔ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) |
23 |
22
|
rabbii |
⊢ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑦 ∈ 𝐵 ∣ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 } |
24 |
|
df-rab |
⊢ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) } |
25 |
23 24
|
eqtri |
⊢ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) } |
26 |
|
nfv |
⊢ Ⅎ 𝑖 𝐾 ∈ HL |
27 |
26 9
|
nfan |
⊢ Ⅎ 𝑖 ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) |
28 |
|
rspa |
⊢ ( ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 ) |
29 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
30 |
1 4
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐵 ) |
31 |
29 30
|
sylan |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐵 ) |
32 |
|
eleq1a |
⊢ ( ( ⊥ ‘ 𝑆 ) ∈ 𝐵 → ( 𝑦 = ( ⊥ ‘ 𝑆 ) → 𝑦 ∈ 𝐵 ) ) |
33 |
31 32
|
syl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) → 𝑦 ∈ 𝐵 ) ) |
34 |
33
|
pm4.71rd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ) ) |
35 |
1 4
|
opcon2b |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑆 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ) |
36 |
29 35
|
syl3an1 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ) |
37 |
36
|
3expa |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ) |
38 |
|
eqcom |
⊢ ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 ) |
39 |
37 38
|
bitr3di |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) |
40 |
39
|
pm5.32da |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) ) |
41 |
34 40
|
bitrd |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) ) |
42 |
28 41
|
sylan2 |
⊢ ( ( 𝐾 ∈ HL ∧ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) ) |
43 |
42
|
anassrs |
⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) ) |
44 |
27 43
|
rexbida |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) ) |
45 |
|
r19.42v |
⊢ ( ∃ 𝑖 ∈ 𝐼 ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) |
46 |
44 45
|
bitr2di |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ) ) |
47 |
46
|
abbidv |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) } = { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) } ) |
48 |
|
eqeq1 |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ 𝑥 = ( ⊥ ‘ 𝑆 ) ) ) |
49 |
48
|
rexbidv |
⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) ) ) |
50 |
49
|
cbvabv |
⊢ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } |
51 |
47 50
|
eqtrdi |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) |
52 |
25 51
|
eqtrid |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) |
53 |
52
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) = ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) |
54 |
53
|
fveq2d |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) ) |
55 |
18 54
|
eqtrd |
⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) ) |