Step | Hyp | Ref
| Expression |
1 | | vex 3402 |
. . . . . 6
⊢ 𝑦 ∈ V |
2 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑆 ↔ 𝑦 = 𝑆)) |
3 | 2 | rexbidv 3207 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (∃𝑖 ∈ 𝐼 𝑥 = 𝑆 ↔ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆)) |
4 | 1, 3 | elab 3573 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆} ↔ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆) |
5 | | nfra1 3131 |
. . . . . 6
⊢
Ⅎ𝑖∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 |
6 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑖 𝑦 ∈ 𝐵 |
7 | | rsp 3118 |
. . . . . . 7
⊢
(∀𝑖 ∈
𝐼 𝑆 ∈ 𝐵 → (𝑖 ∈ 𝐼 → 𝑆 ∈ 𝐵)) |
8 | | eleq1a 2828 |
. . . . . . 7
⊢ (𝑆 ∈ 𝐵 → (𝑦 = 𝑆 → 𝑦 ∈ 𝐵)) |
9 | 7, 8 | syl6 35 |
. . . . . 6
⊢
(∀𝑖 ∈
𝐼 𝑆 ∈ 𝐵 → (𝑖 ∈ 𝐼 → (𝑦 = 𝑆 → 𝑦 ∈ 𝐵))) |
10 | 5, 6, 9 | rexlimd 3227 |
. . . . 5
⊢
(∀𝑖 ∈
𝐼 𝑆 ∈ 𝐵 → (∃𝑖 ∈ 𝐼 𝑦 = 𝑆 → 𝑦 ∈ 𝐵)) |
11 | 4, 10 | syl5bi 245 |
. . . 4
⊢
(∀𝑖 ∈
𝐼 𝑆 ∈ 𝐵 → (𝑦 ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆} → 𝑦 ∈ 𝐵)) |
12 | 11 | ssrdv 3883 |
. . 3
⊢
(∀𝑖 ∈
𝐼 𝑆 ∈ 𝐵 → {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆} ⊆ 𝐵) |
13 | | glbcon.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
14 | | glbcon.u |
. . . 4
⊢ 𝑈 = (lub‘𝐾) |
15 | | glbcon.g |
. . . 4
⊢ 𝐺 = (glb‘𝐾) |
16 | | glbcon.o |
. . . 4
⊢ ⊥ =
(oc‘𝐾) |
17 | 13, 14, 15, 16 | glbconN 37014 |
. . 3
⊢ ((𝐾 ∈ HL ∧ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆} ⊆ 𝐵) → (𝐺‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}) = ( ⊥ ‘(𝑈‘{𝑦 ∈ 𝐵 ∣ ( ⊥ ‘𝑦) ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}}))) |
18 | 12, 17 | sylan2 596 |
. 2
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝐺‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}) = ( ⊥ ‘(𝑈‘{𝑦 ∈ 𝐵 ∣ ( ⊥ ‘𝑦) ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}}))) |
19 | | fvex 6687 |
. . . . . . . 8
⊢ ( ⊥
‘𝑦) ∈
V |
20 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑥 = ( ⊥ ‘𝑦) → (𝑥 = 𝑆 ↔ ( ⊥ ‘𝑦) = 𝑆)) |
21 | 20 | rexbidv 3207 |
. . . . . . . 8
⊢ (𝑥 = ( ⊥ ‘𝑦) → (∃𝑖 ∈ 𝐼 𝑥 = 𝑆 ↔ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆)) |
22 | 19, 21 | elab 3573 |
. . . . . . 7
⊢ (( ⊥
‘𝑦) ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆} ↔ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆) |
23 | 22 | rabbii 3374 |
. . . . . 6
⊢ {𝑦 ∈ 𝐵 ∣ ( ⊥ ‘𝑦) ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}} = {𝑦 ∈ 𝐵 ∣ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆} |
24 | | df-rab 3062 |
. . . . . 6
⊢ {𝑦 ∈ 𝐵 ∣ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆)} |
25 | 23, 24 | eqtri 2761 |
. . . . 5
⊢ {𝑦 ∈ 𝐵 ∣ ( ⊥ ‘𝑦) ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}} = {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆)} |
26 | | nfv 1921 |
. . . . . . . . . 10
⊢
Ⅎ𝑖 𝐾 ∈ HL |
27 | 26, 5 | nfan 1906 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) |
28 | | rspa 3119 |
. . . . . . . . . . 11
⊢
((∀𝑖 ∈
𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼) → 𝑆 ∈ 𝐵) |
29 | | hlop 36999 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
30 | 13, 16 | opoccl 36831 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ OP ∧ 𝑆 ∈ 𝐵) → ( ⊥ ‘𝑆) ∈ 𝐵) |
31 | 29, 30 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵) → ( ⊥ ‘𝑆) ∈ 𝐵) |
32 | | eleq1a 2828 |
. . . . . . . . . . . . . 14
⊢ (( ⊥
‘𝑆) ∈ 𝐵 → (𝑦 = ( ⊥ ‘𝑆) → 𝑦 ∈ 𝐵)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵) → (𝑦 = ( ⊥ ‘𝑆) → 𝑦 ∈ 𝐵)) |
34 | 33 | pm4.71rd 566 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵) → (𝑦 = ( ⊥ ‘𝑆) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 = ( ⊥ ‘𝑆)))) |
35 | 13, 16 | opcon2b 36834 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ OP ∧ 𝑆 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑆 = ( ⊥ ‘𝑦) ↔ 𝑦 = ( ⊥ ‘𝑆))) |
36 | 29, 35 | syl3an1 1164 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑆 = ( ⊥ ‘𝑦) ↔ 𝑦 = ( ⊥ ‘𝑆))) |
37 | 36 | 3expa 1119 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑆 = ( ⊥ ‘𝑦) ↔ 𝑦 = ( ⊥ ‘𝑆))) |
38 | | eqcom 2745 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = ( ⊥ ‘𝑦) ↔ ( ⊥ ‘𝑦) = 𝑆) |
39 | 37, 38 | bitr3di 289 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑦 = ( ⊥ ‘𝑆) ↔ ( ⊥ ‘𝑦) = 𝑆)) |
40 | 39 | pm5.32da 582 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ∧ 𝑦 = ( ⊥ ‘𝑆)) ↔ (𝑦 ∈ 𝐵 ∧ ( ⊥ ‘𝑦) = 𝑆))) |
41 | 34, 40 | bitrd 282 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵) → (𝑦 = ( ⊥ ‘𝑆) ↔ (𝑦 ∈ 𝐵 ∧ ( ⊥ ‘𝑦) = 𝑆))) |
42 | 28, 41 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ (∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼)) → (𝑦 = ( ⊥ ‘𝑆) ↔ (𝑦 ∈ 𝐵 ∧ ( ⊥ ‘𝑦) = 𝑆))) |
43 | 42 | anassrs 471 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) → (𝑦 = ( ⊥ ‘𝑆) ↔ (𝑦 ∈ 𝐵 ∧ ( ⊥ ‘𝑦) = 𝑆))) |
44 | 27, 43 | rexbida 3228 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (∃𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘𝑆) ↔ ∃𝑖 ∈ 𝐼 (𝑦 ∈ 𝐵 ∧ ( ⊥ ‘𝑦) = 𝑆))) |
45 | | r19.42v 3254 |
. . . . . . . 8
⊢
(∃𝑖 ∈
𝐼 (𝑦 ∈ 𝐵 ∧ ( ⊥ ‘𝑦) = 𝑆) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆)) |
46 | 44, 45 | bitr2di 291 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ∧ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆) ↔ ∃𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘𝑆))) |
47 | 46 | abbidv 2802 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆)} = {𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘𝑆)}) |
48 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑦 = ( ⊥ ‘𝑆) ↔ 𝑥 = ( ⊥ ‘𝑆))) |
49 | 48 | rexbidv 3207 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘𝑆) ↔ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆))) |
50 | 49 | cbvabv 2806 |
. . . . . 6
⊢ {𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘𝑆)} = {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)} |
51 | 47, 50 | eqtrdi 2789 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → {𝑦 ∣ (𝑦 ∈ 𝐵 ∧ ∃𝑖 ∈ 𝐼 ( ⊥ ‘𝑦) = 𝑆)} = {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)}) |
52 | 25, 51 | syl5eq 2785 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → {𝑦 ∈ 𝐵 ∣ ( ⊥ ‘𝑦) ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}} = {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)}) |
53 | 52 | fveq2d 6678 |
. . 3
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝑈‘{𝑦 ∈ 𝐵 ∣ ( ⊥ ‘𝑦) ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}}) = (𝑈‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)})) |
54 | 53 | fveq2d 6678 |
. 2
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → ( ⊥ ‘(𝑈‘{𝑦 ∈ 𝐵 ∣ ( ⊥ ‘𝑦) ∈ {𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}})) = ( ⊥ ‘(𝑈‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)}))) |
55 | 18, 54 | eqtrd 2773 |
1
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝐺‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}) = ( ⊥ ‘(𝑈‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)}))) |