Metamath Proof Explorer

Theorem islpln5

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 24-Jun-2012)

Ref Expression
Hypotheses islpln5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
islpln5.l ⊢ ≤ = ( le ‘ 𝐾 )
islpln5.j ⊢ ∨ = ( join ‘ 𝐾 )
islpln5.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
islpln5.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion islpln5 ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )

Proof

Step Hyp Ref Expression
1 islpln5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 islpln5.l ⊢ ≤ = ( le ‘ 𝐾 )
3 islpln5.j ⊢ ∨ = ( join ‘ 𝐾 )
4 islpln5.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 islpln5.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
7 1 2 3 4 6 5 islpln3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑦 ∈ ( LLines ‘ 𝐾 ) ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) )
8 df-rex ⊢ ( ∃ 𝑦 ∈ ( LLines ‘ 𝐾 ) ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) )
9 r19.41v ⊢ ( ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ( ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
10 an13 ⊢ ( ( ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ) )
11 9 10 bitri ⊢ ( ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ) )
12 11 exbii ⊢ ( ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑦 ( 𝑦 = ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ) )
13 ovex ⊢ ( 𝑝 ∨ 𝑞 ) ∈ V
14 an12 ⊢ ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) )
15 eleq1 ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( 𝑦 ∈ 𝐵 ↔ ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ) )
16 breq2 ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( 𝑟 ≤ 𝑦 ↔ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) )
17 16 notbid ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( ¬ 𝑟 ≤ 𝑦 ↔ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) )
18 oveq1 ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( 𝑦 ∨ 𝑟 ) = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) )
19 18 eqeq2d ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( 𝑋 = ( 𝑦 ∨ 𝑟 ) ↔ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) )
20 17 19 anbi12d ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ↔ ( ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
21 20 anbi2d ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
22 3anass ⊢ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
23 21 22 bitr4di ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
24 15 23 anbi12d ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
25 14 24 syl5bb ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( ( 𝑝 ≠ 𝑞 ∧ ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
26 25 rexbidv ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ↔ ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
27 r19.42v ⊢ ( ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ↔ ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) )
28 r19.42v ⊢ ( ∃ 𝑟 ∈ 𝐴 ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
29 26 27 28 3bitr3g ⊢ ( 𝑦 = ( 𝑝 ∨ 𝑞 ) → ( ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
30 13 29 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = ( 𝑝 ∨ 𝑞 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
31 12 30 bitri ⊢ ( ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
32 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
33 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → 𝑝 ∈ 𝐴 )
34 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → 𝑞 ∈ 𝐴 )
35 1 3 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 )
36 32 33 34 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 )
37 36 biantrurd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑝 ∨ 𝑞 ) ∈ 𝐵 ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) ) )
38 31 37 bitr4id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
39 38 2rexbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
40 rexcom4 ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑦 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
41 40 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑦 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
42 rexcom4 ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑦 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑦 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
43 41 42 bitri ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑦 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑦 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
44 39 43 bitr3di ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ∃ 𝑦 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ) )
45 rexcom ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
46 45 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
47 rexcom ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
48 46 47 bitri ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
49 1 3 4 6 islln2 ⊢ ( 𝐾 ∈ HL → ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ) )
50 49 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ) )
51 50 anbi1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) )
52 r19.42v ⊢ ( ∃ 𝑝 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
53 r19.42v ⊢ ( ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
54 53 rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
55 an32 ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
56 52 54 55 3bitr4ri ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) )
57 51 56 bitrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ) )
58 57 rexbidv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ) )
59 48 58 bitr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) )
60 r19.42v ⊢ ( ∃ 𝑟 ∈ 𝐴 ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ↔ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) )
61 59 60 bitrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) )
62 61 exbidv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑦 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( ( 𝑦 ∈ 𝐵 ∧ ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑦 = ( 𝑝 ∨ 𝑞 ) ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) )
63 44 62 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( LLines ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ) ) )
64 8 63 bitr4id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ ( LLines ‘ 𝐾 ) ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑟 ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
65 7 64 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑃 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )