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

Metamath Proof Explorer

Theorem 3dim0

Description: There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
5 1 4 3 athgt ⊢ ( 𝐾 ∈ HL → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
6 df-3an ⊢ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
7 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → 𝐾 ∈ HL )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 1 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
10 9 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
11 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → 𝑟 ∈ 𝐴 )
12 8 2 1 4 3 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ 𝐴 ) → ( ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
13 7 10 11 12 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ↔ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
14 13 anbi2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
15 7 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → 𝐾 ∈ Lat )
16 8 3 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
17 16 ad2antlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
18 8 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
19 15 10 17 18 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
20 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ 𝐴 )
21 8 2 1 4 3 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑠 ∈ 𝐴 ) → ( ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
22 7 19 20 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
23 14 22 anbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
24 6 23 bitrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
25 24 rexbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ∃ 𝑠 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
26 r19.42v ⊢ ( ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
27 anass ⊢ ( ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
28 26 27 bitri ⊢ ( ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
29 25 28 bitrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ∃ 𝑠 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
30 29 rexbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
31 r19.42v ⊢ ( ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
32 30 31 bitrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
33 1 4 3 atcvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑝 ≠ 𝑞 ↔ 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) ) )
34 33 anbi1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ↔ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
35 32 34 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
36 35 3expb ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
37 36 2rexbidva ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ( ⋖ ‘ 𝐾 ) ( 𝑝 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
38 5 37 mpbird ⊢ ( 𝐾 ∈ HL → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )