Metamath Proof Explorer

Theorem islvol5

Description: The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012)

Ref Expression
Hypotheses islvol5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
islvol5.l ⊢ ≤ = ( le ‘ 𝐾 )
islvol5.j ⊢ ∨ = ( join ‘ 𝐾 )
islvol5.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
islvol5.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion islvol5 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 islvol5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 islvol5.l ⊢ ≤ = ( le ‘ 𝐾 )
3 islvol5.j ⊢ ∨ = ( join ‘ 𝐾 )
4 islvol5.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 islvol5.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
6 eqid ⊢ ( LPlanes ‘ 𝐾 ) = ( LPlanes ‘ 𝐾 )
7 1 2 3 4 6 5 islvol3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) )
8 df-rex ⊢ ( ∃ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) )
9 r19.41v ⊢ ( ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
10 df-3an ⊢ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
11 10 anbi2i ⊢ ( ( ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
12 an13 ⊢ ( ( ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ) )
13 11 12 bitri ⊢ ( ( ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ) )
14 9 13 bitri ⊢ ( ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ) )
15 14 exbii ⊢ ( ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑦 ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ) )
16 ovex ⊢ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ V
17 an12 ⊢ ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) )
18 eleq1 ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( 𝑦 ∈ 𝐵 ↔ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ) )
19 breq2 ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( 𝑠 ≤ 𝑦 ↔ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
20 19 notbid ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( ¬ 𝑠 ≤ 𝑦 ↔ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
21 oveq1 ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( 𝑦 ∨ 𝑠 ) = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) )
22 21 eqeq2d ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( 𝑋 = ( 𝑦 ∨ 𝑠 ) ↔ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
23 20 22 anbi12d ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ↔ ( ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
24 23 anbi2d ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
25 anass ⊢ ( ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
26 df-3an ⊢ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
27 26 bicomi ⊢ ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
28 27 anbi1i ⊢ ( ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
29 25 28 bitr3i ⊢ ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
30 24 29 bitrdi ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
31 18 30 anbi12d ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( ( 𝑦 ∈ 𝐵 ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ↔ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
32 17 31 syl5bb ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ↔ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
33 32 rexbidv ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
34 r19.42v ⊢ ( ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ↔ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) )
35 r19.42v ⊢ ( ∃ 𝑠 ∈ 𝐴 ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ↔ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
36 33 34 35 3bitr3g ⊢ ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) → ( ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ↔ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
37 16 36 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∧ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) ) ↔ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
38 15 37 bitri ⊢ ( ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
39 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
40 39 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ Lat )
41 simplll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ HL )
42 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑝 ∈ 𝐴 )
43 simplrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑞 ∈ 𝐴 )
44 1 3 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 )
45 41 42 43 44 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 )
46 1 4 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵 )
47 46 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐵 )
48 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 )
49 40 45 47 48 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 )
50 49 biantrurd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∈ 𝐵 ∧ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
51 38 50 bitr4id ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
52 51 rexbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
53 52 2rexbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
54 rexcom4 ⊢ ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
55 54 rexbii ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
56 rexcom4 ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑦 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
57 55 56 bitri ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑦 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
58 57 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑦 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
59 rexcom4 ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑦 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑦 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
60 58 59 bitri ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑦 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑦 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
61 53 60 bitr3di ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ∃ 𝑦 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
62 rexcom ⊢ ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
63 62 rexbii ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
64 rexcom ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
65 63 64 bitri ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
66 65 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
67 rexcom ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
68 66 67 bitri ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
69 1 2 3 4 6 islpln2 ⊢ ( 𝐾 ∈ HL → ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
70 69 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
71 70 anbi1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) )
72 r19.42v ⊢ ( ∃ 𝑝 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
73 r19.42v ⊢ ( ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
74 73 rexbii ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
75 r19.42v ⊢ ( ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
76 74 75 bitri ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
77 76 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
78 an32 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
79 72 77 78 3bitr4ri ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
80 71 79 bitrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
81 80 rexbidv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
82 68 81 bitr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) )
83 r19.42v ⊢ ( ∃ 𝑠 ∈ 𝐴 ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ↔ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) )
84 82 83 bitrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) )
85 84 exbidv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑦 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑦 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) )
86 61 85 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ) ) )
87 8 86 bitr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑠 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑠 ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
88 7 87 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) )