This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3dim1lem5

Description: Lemma for 3dim1 . (Contributed by NM, 26-Jul-2012)

Ref Expression
Hypotheses 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3dim1lem5 ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 neeq2 ⊢ ( 𝑞 = 𝑢 → ( 𝑃 ≠ 𝑞 ↔ 𝑃 ≠ 𝑢 ) )
5 oveq2 ⊢ ( 𝑞 = 𝑢 → ( 𝑃 ∨ 𝑞 ) = ( 𝑃 ∨ 𝑢 ) )
6 5 breq2d ⊢ ( 𝑞 = 𝑢 → ( 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ↔ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) )
7 6 notbid ⊢ ( 𝑞 = 𝑢 → ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ↔ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) )
8 5 oveq1d ⊢ ( 𝑞 = 𝑢 → ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) = ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) )
9 8 breq2d ⊢ ( 𝑞 = 𝑢 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ↔ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) )
10 9 notbid ⊢ ( 𝑞 = 𝑢 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) )
11 4 7 10 3anbi123d ⊢ ( 𝑞 = 𝑢 → ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) ) )
12 breq1 ⊢ ( 𝑟 = 𝑣 → ( 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ↔ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ) )
13 12 notbid ⊢ ( 𝑟 = 𝑣 → ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ↔ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ) )
14 oveq2 ⊢ ( 𝑟 = 𝑣 → ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) = ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) )
15 14 breq2d ⊢ ( 𝑟 = 𝑣 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ↔ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) )
16 15 notbid ⊢ ( 𝑟 = 𝑣 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) )
17 13 16 3anbi23d ⊢ ( 𝑟 = 𝑣 → ( ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) ↔ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
18 breq1 ⊢ ( 𝑠 = 𝑤 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ↔ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) )
19 18 notbid ⊢ ( 𝑠 = 𝑤 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ↔ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) )
20 19 3anbi3d ⊢ ( 𝑠 = 𝑤 → ( ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ↔ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) )
21 11 17 20 rspc3ev ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )