Proof of Theorem lhpexle3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lhpex1.l | . . . . 5
⊢  ≤ =
(le‘𝐾) | 
| 2 |  | lhpex1.a | . . . . 5
⊢ 𝐴 = (Atoms‘𝐾) | 
| 3 |  | lhpex1.h | . . . . 5
⊢ 𝐻 = (LHyp‘𝐾) | 
| 4 | 1, 2, 3 | lhpexle2 40012 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌)) | 
| 5 |  | 3anass 1095 | . . . . 5
⊢ ((𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ↔ (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌))) | 
| 6 | 5 | rexbii 3094 | . . . 4
⊢
(∃𝑝 ∈
𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌))) | 
| 7 | 4, 6 | sylib 218 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌))) | 
| 8 | 1, 2, 3 | lhpexle2 40012 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍)) | 
| 9 | 8 | adantr 480 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍)) | 
| 10 |  | 3anass 1095 | . . . . . . 7
⊢ ((𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ↔ (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍))) | 
| 11 | 10 | rexbii 3094 | . . . . . 6
⊢
(∃𝑝 ∈
𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍))) | 
| 12 | 9, 11 | sylib 218 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍))) | 
| 13 | 1, 2, 3 | lhpexle2 40012 | . . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍)) | 
| 14 |  | 3anass 1095 | . . . . . . . . . . 11
⊢ ((𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ↔ (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) | 
| 15 | 14 | rexbii 3094 | . . . . . . . . . 10
⊢
(∃𝑝 ∈
𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) | 
| 16 | 13, 15 | sylib 218 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) | 
| 17 | 16 | 3ad2ant1 1134 | . . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) | 
| 18 |  | simpl1 1192 | . . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 19 |  | simpl3l 1229 | . . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → 𝑌 ∈ 𝐴) | 
| 20 |  | simpl2l 1227 | . . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → 𝑍 ∈ 𝐴) | 
| 21 |  | simprl 771 | . . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → 𝑋 ∈ 𝐴) | 
| 22 |  | simpl3r 1230 | . . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → 𝑌 ≤ 𝑊) | 
| 23 |  | simpl2r 1228 | . . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → 𝑍 ≤ 𝑊) | 
| 24 |  | simprr 773 | . . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → 𝑋 ≤ 𝑊) | 
| 25 | 1, 2, 3 | lhpexle3lem 40013 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ∧ 𝑋 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋))) | 
| 26 | 18, 19, 20, 21, 22, 23, 24, 25 | syl133anc 1395 | . . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋))) | 
| 27 |  | df-3an 1089 | . . . . . . . . . . . 12
⊢ ((𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋) ↔ ((𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋)) | 
| 28 | 27 | anbi2i 623 | . . . . . . . . . . 11
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋)) ↔ (𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋))) | 
| 29 |  | 3anass 1095 | . . . . . . . . . . 11
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋) ↔ (𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋))) | 
| 30 | 28, 29 | bitr4i 278 | . . . . . . . . . 10
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋)) ↔ (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋)) | 
| 31 | 30 | rexbii 3094 | . . . . . . . . 9
⊢
(∃𝑝 ∈
𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍 ∧ 𝑝 ≠ 𝑋)) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋)) | 
| 32 | 26, 31 | sylib 218 | . . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋)) | 
| 33 | 17, 32 | lhpexle1lem 40009 | . . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋)) | 
| 34 |  | an31 648 | . . . . . . . . . 10
⊢ (((𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋) ↔ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌)) | 
| 35 | 34 | anbi2i 623 | . . . . . . . . 9
⊢ ((𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋)) ↔ (𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌))) | 
| 36 |  | 3anass 1095 | . . . . . . . . 9
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌) ↔ (𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌))) | 
| 37 | 35, 29, 36 | 3bitr4i 303 | . . . . . . . 8
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋) ↔ (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌)) | 
| 38 | 37 | rexbii 3094 | . . . . . . 7
⊢
(∃𝑝 ∈
𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑋) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌)) | 
| 39 | 33, 38 | sylib 218 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌)) | 
| 40 | 39 | 3expa 1119 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊)) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌)) | 
| 41 | 12, 40 | lhpexle1lem 40009 | . . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌)) | 
| 42 |  | an32 646 | . . . . . . 7
⊢ (((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌) ↔ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍)) | 
| 43 | 42 | anbi2i 623 | . . . . . 6
⊢ ((𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌)) ↔ (𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍))) | 
| 44 |  | 3anass 1095 | . . . . . 6
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍) ↔ (𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍))) | 
| 45 | 43, 36, 44 | 3bitr4i 303 | . . . . 5
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌) ↔ (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍)) | 
| 46 | 45 | rexbii 3094 | . . . 4
⊢
(∃𝑝 ∈
𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑍) ∧ 𝑝 ≠ 𝑌) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍)) | 
| 47 | 41, 46 | sylib 218 | . . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑍 ∈ 𝐴 ∧ 𝑍 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍)) | 
| 48 | 7, 47 | lhpexle1lem 40009 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍)) | 
| 49 |  | df-3an 1089 | . . . . 5
⊢ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍) ↔ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍)) | 
| 50 | 49 | anbi2i 623 | . . . 4
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍)) ↔ (𝑝 ≤ 𝑊 ∧ ((𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍))) | 
| 51 | 44, 50 | bitr4i 278 | . . 3
⊢ ((𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍) ↔ (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) | 
| 52 | 51 | rexbii 3094 | . 2
⊢
(∃𝑝 ∈
𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌) ∧ 𝑝 ≠ 𝑍) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) | 
| 53 | 48, 52 | sylib 218 | 1
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) |