Metamath Proof Explorer

Theorem lnincplng

Description: If two lines A and B intersect, then B is in a plane defined by A and any point of B . Lemma 9.22 of Schwabhauser p. 74. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
lnincplng.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
lnincplng.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
lnincplng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
lnincplng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
lnincplng.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
lnincplng.2 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = { 𝑌 } )
Assertion lnincplng ( 𝜑 → 𝐵 ⊆ ( 𝐴 𝐸 𝑋 ) )

Proof

Step Hyp Ref Expression
1 plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
5 plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 lnincplng.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 lnincplng.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
8 lnincplng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9 lnincplng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10 lnincplng.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
11 lnincplng.2 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = { 𝑌 } )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 = 𝑋 ) → 𝑧 = 𝑋 )
13 1 3 2 5 7 8 tglnpt ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
14 10 neneqd ⊢ ( 𝜑 → ¬ 𝑋 = 𝑌 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
17 15 16 elind ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
18 11 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) = { 𝑌 } )
19 17 18 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ { 𝑌 } )
20 19 elsnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 = 𝑌 )
21 14 20 mtand ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
22 13 21 eldifd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
23 1 2 3 4 5 6 22 elplngid ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐸 𝑋 ) )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 = 𝑋 ) → 𝑋 ∈ ( 𝐴 𝐸 𝑋 ) )
25 12 24 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 = 𝑋 ) → 𝑧 ∈ ( 𝐴 𝐸 𝑋 ) )
26 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 = 𝑌 ) → 𝑧 = 𝑌 )
27 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 = 𝑌 ) → 𝐺 ∈ TarskiG )
28 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 = 𝑌 ) → 𝐴 ∈ ran 𝐿 )
29 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 = 𝑌 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
30 1 2 3 4 27 28 29 elplnglnid ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 = 𝑌 ) → 𝐴 ⊆ ( 𝐴 𝐸 𝑋 ) )
31 snidg ⊢ ( 𝑌 ∈ 𝑃 → 𝑌 ∈ { 𝑌 } )
32 9 31 syl ⊢ ( 𝜑 → 𝑌 ∈ { 𝑌 } )
33 32 11 eleqtrrd ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 ∩ 𝐵 ) )
34 33 elin1d ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
35 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 = 𝑌 ) → 𝑌 ∈ 𝐴 )
36 30 35 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 = 𝑌 ) → 𝑌 ∈ ( 𝐴 𝐸 𝑋 ) )
37 26 36 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 = 𝑌 ) → 𝑧 ∈ ( 𝐴 𝐸 𝑋 ) )
38 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑧 ≠ 𝑌 )
39 38 neneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ¬ 𝑧 = 𝑌 )
40 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
41 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑧 ∈ 𝐵 )
42 41 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 )
43 40 42 elind ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ( 𝐴 ∩ 𝐵 ) )
44 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) = { 𝑌 } )
45 43 44 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ { 𝑌 } )
46 45 elsnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 = 𝑌 )
47 39 46 mtand ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ¬ 𝑧 ∈ 𝐴 )
48 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝐺 ∈ TarskiG )
49 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝐴 ∈ ran 𝐿 )
50 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝐵 ∈ ran 𝐿 )
51 1 3 2 48 50 41 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑧 ∈ 𝑃 )
52 eleq1w ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ↔ 𝑐 ∈ ( 𝑃 ∖ 𝐴 ) ) )
53 eleq1w ⊢ ( 𝑏 = 𝑑 → ( 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ↔ 𝑑 ∈ ( 𝑃 ∖ 𝐴 ) ) )
54 52 53 bi2anan9 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ↔ ( 𝑐 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑑 ∈ ( 𝑃 ∖ 𝐴 ) ) ) )
55 eleq1w ⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) )
56 55 cbvrexvw ⊢ ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) )
57 oveq12 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 𝐼 𝑏 ) = ( 𝑐 𝐼 𝑑 ) )
58 57 eleq2d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) )
59 58 rexbidv ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) )
60 56 59 bitrid ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) )
61 54 60 anbi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑐 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑑 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) ) )
62 61 cbvopabv ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑑 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) }
63 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑋 ∈ 𝑃 )
64 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑌 ∈ 𝐴 )
65 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑌 ∈ 𝑃 )
66 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑧 ≠ 𝑋 )
67 33 elin2d ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
68 67 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑌 ∈ 𝐵 )
69 66 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑋 ≠ 𝑧 )
70 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑋 ∈ 𝐵 )
71 1 2 3 48 63 51 69 69 50 70 41 tglinethru ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝐵 = ( 𝑋 𝐿 𝑧 ) )
72 68 71 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑌 ∈ ( 𝑋 𝐿 𝑧 ) )
73 1 2 3 48 51 63 65 66 72 lncom ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑌 ∈ ( 𝑧 𝐿 𝑋 ) )
74 73 orcd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ( 𝑌 ∈ ( 𝑧 𝐿 𝑋 ) ∨ 𝑧 = 𝑋 ) )
75 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
76 1 2 3 48 49 51 62 63 64 74 75 colhp ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ( 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ↔ ( 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ∧ ¬ 𝑧 ∈ 𝐴 ) ) )
77 47 76 mpbiran2d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ( 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ↔ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) )
78 77 biimpar ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ) → 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
79 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
80 51 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → 𝑧 ∈ 𝑃 )
81 63 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → 𝑋 ∈ 𝑃 )
82 64 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → 𝑌 ∈ 𝐴 )
83 47 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → ¬ 𝑧 ∈ 𝐴 )
84 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ¬ 𝑋 ∈ 𝐴 )
85 84 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → ¬ 𝑋 ∈ 𝐴 )
86 48 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → 𝐺 ∈ TarskiG )
87 65 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → 𝑌 ∈ 𝑃 )
88 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) )
89 1 79 2 86 81 87 80 88 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → 𝑌 ∈ ( 𝑧 𝐼 𝑋 ) )
90 1 79 2 62 80 81 82 83 85 89 islnoppd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) → 𝑧 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 )
91 1 2 3 5 13 9 10 10 7 8 67 tglinethru ⊢ ( 𝜑 → 𝐵 = ( 𝑋 𝐿 𝑌 ) )
92 91 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝐵 = ( 𝑋 𝐿 𝑌 ) )
93 41 92 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) )
94 1 2 75 63 65 51 48 63 3 93 lnhl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ( 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑋 ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ) )
95 78 90 94 orim12da ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ( 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑧 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ) )
96 95 olcd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ( 𝑧 ∈ 𝐴 ∨ ( 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑧 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ) ) )
97 3orass ⊢ ( ( 𝑧 ∈ 𝐴 ∨ 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑧 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∨ ( 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑧 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ) ) )
98 96 97 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ( 𝑧 ∈ 𝐴 ∨ 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑧 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ) )
99 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
100 1 2 3 4 48 49 99 62 51 elplng ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → ( 𝑧 ∈ ( 𝐴 𝐸 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑧 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ) ) )
101 98 100 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑌 ) → 𝑧 ∈ ( 𝐴 𝐸 𝑋 ) )
102 37 101 pm2.61dane ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) → 𝑧 ∈ ( 𝐴 𝐸 𝑋 ) )
103 25 102 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐴 𝐸 𝑋 ) )
104 103 ex ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ( 𝐴 𝐸 𝑋 ) ) )
105 104 ssrdv ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐴 𝐸 𝑋 ) )