Proof of Theorem pmapglb2N
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hlop 39363 | . . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | 
| 2 |  | pmapglb2.g | . . . . . . . 8
⊢ 𝐺 = (glb‘𝐾) | 
| 3 |  | eqid 2737 | . . . . . . . 8
⊢
(1.‘𝐾) =
(1.‘𝐾) | 
| 4 | 2, 3 | glb0N 39194 | . . . . . . 7
⊢ (𝐾 ∈ OP → (𝐺‘∅) =
(1.‘𝐾)) | 
| 5 | 4 | fveq2d 6910 | . . . . . 6
⊢ (𝐾 ∈ OP → (𝑀‘(𝐺‘∅)) = (𝑀‘(1.‘𝐾))) | 
| 6 |  | pmapglb2.a | . . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) | 
| 7 |  | pmapglb2.m | . . . . . . 7
⊢ 𝑀 = (pmap‘𝐾) | 
| 8 | 3, 6, 7 | pmap1N 39769 | . . . . . 6
⊢ (𝐾 ∈ OP → (𝑀‘(1.‘𝐾)) = 𝐴) | 
| 9 | 5, 8 | eqtrd 2777 | . . . . 5
⊢ (𝐾 ∈ OP → (𝑀‘(𝐺‘∅)) = 𝐴) | 
| 10 | 1, 9 | syl 17 | . . . 4
⊢ (𝐾 ∈ HL → (𝑀‘(𝐺‘∅)) = 𝐴) | 
| 11 |  | 2fveq3 6911 | . . . . 5
⊢ (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝑀‘(𝐺‘∅))) | 
| 12 |  | riin0 5082 | . . . . 5
⊢ (𝑆 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥)) = 𝐴) | 
| 13 | 11, 12 | eqeq12d 2753 | . . . 4
⊢ (𝑆 = ∅ → ((𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) ↔ (𝑀‘(𝐺‘∅)) = 𝐴)) | 
| 14 | 10, 13 | syl5ibrcom 247 | . . 3
⊢ (𝐾 ∈ HL → (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) | 
| 15 | 14 | adantr 480 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) | 
| 16 |  | pmapglb2.b | . . . . 5
⊢ 𝐵 = (Base‘𝐾) | 
| 17 | 16, 2, 7 | pmapglb 39772 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝑀‘(𝐺‘𝑆)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) | 
| 18 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) | 
| 19 |  | simpll 767 | . . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL) | 
| 20 |  | ssel2 3978 | . . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) | 
| 21 | 20 | adantll 714 | . . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) | 
| 22 | 16, 6, 7 | pmapssat 39761 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑥 ∈ 𝐵) → (𝑀‘𝑥) ⊆ 𝐴) | 
| 23 | 19, 21, 22 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑀‘𝑥) ⊆ 𝐴) | 
| 24 | 18, 23 | jca 511 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴)) | 
| 25 | 24 | ex 412 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴))) | 
| 26 | 25 | eximdv 1917 | . . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴))) | 
| 27 |  | n0 4353 | . . . . . . . 8
⊢ (𝑆 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑆) | 
| 28 |  | df-rex 3071 | . . . . . . . 8
⊢
(∃𝑥 ∈
𝑆 (𝑀‘𝑥) ⊆ 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴)) | 
| 29 | 26, 27, 28 | 3imtr4g 296 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 ≠ ∅ → ∃𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴)) | 
| 30 | 29 | 3impia 1118 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → ∃𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) | 
| 31 |  | iinss 5056 | . . . . . 6
⊢
(∃𝑥 ∈
𝑆 (𝑀‘𝑥) ⊆ 𝐴 → ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) | 
| 32 | 30, 31 | syl 17 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) | 
| 33 |  | sseqin2 4223 | . . . . 5
⊢ (∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴 ↔ (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) | 
| 34 | 32, 33 | sylib 218 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) | 
| 35 | 17, 34 | eqtr4d 2780 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥))) | 
| 36 | 35 | 3expia 1122 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 ≠ ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) | 
| 37 | 15, 36 | pm2.61dne 3028 | 1
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥))) |