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

Metamath Proof Explorer

Theorem osumcllem9N

Description: Lemma for osumclN . (Contributed by NM, 24-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses osumcllem.l ⊢ ≤ = ( le ‘ 𝐾 )
osumcllem.j ⊢ ∨ = ( join ‘ 𝐾 )
osumcllem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
osumcllem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
osumcllem.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
osumcllem.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
osumcllem.m ⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
osumcllem.u ⊢ 𝑈 = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) )
Assertion osumcllem9N ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑀 = 𝑋 )

Proof

Step Hyp Ref Expression
1 osumcllem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 osumcllem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 osumcllem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 osumcllem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 osumcllem.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
6 osumcllem.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
7 osumcllem.m ⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
8 osumcllem.u ⊢ 𝑈 = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) )
9 inass ⊢ ( ( ( ⊥ ‘ 𝑋 ) ∩ 𝑈 ) ∩ 𝑀 ) = ( ( ⊥ ‘ 𝑋 ) ∩ ( 𝑈 ∩ 𝑀 ) )
10 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝐾 ∈ HL )
11 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑌 ∈ 𝐶 )
12 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) )
13 1 2 3 4 5 6 7 8 osumcllem3N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑈 ) = 𝑌 )
14 10 11 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑈 ) = 𝑌 )
15 14 ineq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ( ( ⊥ ‘ 𝑋 ) ∩ 𝑈 ) ∩ 𝑀 ) = ( 𝑌 ∩ 𝑀 ) )
16 9 15 eqtr3id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ ( 𝑈 ∩ 𝑀 ) ) = ( 𝑌 ∩ 𝑀 ) )
17 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑋 ∈ 𝐶 )
18 3 6 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ⊆ 𝐴 )
19 10 17 18 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑋 ⊆ 𝐴 )
20 3 6 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ) → 𝑌 ⊆ 𝐴 )
21 10 11 20 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑌 ⊆ 𝐴 )
22 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑋 ≠ ∅ )
23 3 4 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
24 10 19 21 23 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
25 3 5 polssatN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ 𝐴 )
26 10 24 25 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ 𝐴 )
27 3 5 polssatN ⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ⊆ 𝐴 )
28 10 26 27 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ⊆ 𝐴 )
29 8 28 eqsstrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑈 ⊆ 𝐴 )
30 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑝 ∈ 𝑈 )
31 29 30 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑝 ∈ 𝐴 )
32 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) )
33 1 2 3 4 5 6 7 8 osumcllem8N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑌 ∩ 𝑀 ) = ∅ )
34 10 19 21 12 22 31 32 33 syl331anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑌 ∩ 𝑀 ) = ∅ )
35 16 34 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ ( 𝑈 ∩ 𝑀 ) ) = ∅ )
36 35 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( 𝑈 ∩ 𝑀 ) ) ) = ( ⊥ ‘ ∅ ) )
37 3 5 pol0N ⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ∅ ) = 𝐴 )
38 10 37 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ⊥ ‘ ∅ ) = 𝐴 )
39 36 38 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( 𝑈 ∩ 𝑀 ) ) ) = 𝐴 )
40 1 2 3 4 5 6 7 8 osumcllem1N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( 𝑈 ∩ 𝑀 ) = 𝑀 )
41 10 19 21 30 40 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑈 ∩ 𝑀 ) = 𝑀 )
42 39 41 ineq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( 𝑈 ∩ 𝑀 ) ) ) ∩ ( 𝑈 ∩ 𝑀 ) ) = ( 𝐴 ∩ 𝑀 ) )
43 3 5 6 polsubclN ⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∈ 𝐶 )
44 10 26 43 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∈ 𝐶 )
45 8 44 eqeltrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑈 ∈ 𝐶 )
46 3 4 6 paddatclN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑋 + { 𝑝 } ) ∈ 𝐶 )
47 10 17 31 46 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑋 + { 𝑝 } ) ∈ 𝐶 )
48 7 47 eqeltrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑀 ∈ 𝐶 )
49 6 psubclinN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐶 ∧ 𝑀 ∈ 𝐶 ) → ( 𝑈 ∩ 𝑀 ) ∈ 𝐶 )
50 10 45 48 49 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑈 ∩ 𝑀 ) ∈ 𝐶 )
51 1 2 3 4 5 6 7 8 osumcllem2N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝑋 ⊆ ( 𝑈 ∩ 𝑀 ) )
52 10 19 21 30 51 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑋 ⊆ ( 𝑈 ∩ 𝑀 ) )
53 6 5 poml6N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ ( 𝑈 ∩ 𝑀 ) ∈ 𝐶 ) ∧ 𝑋 ⊆ ( 𝑈 ∩ 𝑀 ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( 𝑈 ∩ 𝑀 ) ) ) ∩ ( 𝑈 ∩ 𝑀 ) ) = 𝑋 )
54 10 17 50 52 53 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( 𝑈 ∩ 𝑀 ) ) ) ∩ ( 𝑈 ∩ 𝑀 ) ) = 𝑋 )
55 31 snssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → { 𝑝 } ⊆ 𝐴 )
56 3 4 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ { 𝑝 } ⊆ 𝐴 ) → ( 𝑋 + { 𝑝 } ) ⊆ 𝐴 )
57 10 19 55 56 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑋 + { 𝑝 } ) ⊆ 𝐴 )
58 7 57 eqsstrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑀 ⊆ 𝐴 )
59 sseqin2 ⊢ ( 𝑀 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝑀 ) = 𝑀 )
60 58 59 sylib ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝐴 ∩ 𝑀 ) = 𝑀 )
61 42 54 60 3eqtr3rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑀 = 𝑋 )