Metamath Proof Explorer


Theorem atomli

Description: An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition 3.2.17 of PtakPulmannova p. 66. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1 𝐴C
Assertion atomli ( 𝐵 ∈ HAtoms → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0 } ) )

Proof

Step Hyp Ref Expression
1 atoml.1 𝐴C
2 atelch ( 𝐵 ∈ HAtoms → 𝐵C )
3 chjcl ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵 ) ∈ C )
4 1 2 3 sylancr ( 𝐵 ∈ HAtoms → ( 𝐴 𝐵 ) ∈ C )
5 1 choccli ( ⊥ ‘ 𝐴 ) ∈ C
6 chincl ( ( ( 𝐴 𝐵 ) ∈ C ∧ ( ⊥ ‘ 𝐴 ) ∈ C ) → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ C )
7 4 5 6 sylancl ( 𝐵 ∈ HAtoms → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ C )
8 hatomic ( ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ C ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) )
9 7 8 sylan ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) )
10 atelch ( 𝑥 ∈ HAtoms → 𝑥C )
11 inss2 ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ 𝐴 )
12 sstr ( ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ⊆ ( ⊥ ‘ 𝐴 ) ) → 𝑥 ⊆ ( ⊥ ‘ 𝐴 ) )
13 11 12 mpan2 ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) → 𝑥 ⊆ ( ⊥ ‘ 𝐴 ) )
14 1 pjococi ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) = 𝐴
15 14 oveq1i ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ 𝑥 ) = ( 𝐴 𝑥 )
16 15 ineq1i ( ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ 𝑥 ) ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( 𝐴 𝑥 ) ∩ ( ⊥ ‘ 𝐴 ) )
17 incom ( ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ 𝑥 ) ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ 𝑥 ) )
18 16 17 eqtr3i ( ( 𝐴 𝑥 ) ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ 𝑥 ) )
19 pjoml3 ( ( ( ⊥ ‘ 𝐴 ) ∈ C𝑥C ) → ( 𝑥 ⊆ ( ⊥ ‘ 𝐴 ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ 𝑥 ) ) = 𝑥 ) )
20 5 19 mpan ( 𝑥C → ( 𝑥 ⊆ ( ⊥ ‘ 𝐴 ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ 𝑥 ) ) = 𝑥 ) )
21 20 imp ( ( 𝑥C𝑥 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∨ 𝑥 ) ) = 𝑥 )
22 18 21 syl5eq ( ( 𝑥C𝑥 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( ( 𝐴 𝑥 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 𝑥 )
23 10 13 22 syl2an ( ( 𝑥 ∈ HAtoms ∧ 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) → ( ( 𝐴 𝑥 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 𝑥 )
24 23 ad2ant2lr ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( ( 𝐴 𝑥 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 𝑥 )
25 inss1 ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ⊆ ( 𝐴 𝐵 )
26 sstr ( ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ⊆ ( 𝐴 𝐵 ) ) → 𝑥 ⊆ ( 𝐴 𝐵 ) )
27 25 26 mpan2 ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) → 𝑥 ⊆ ( 𝐴 𝐵 ) )
28 chub1 ( ( 𝐴C𝐵C ) → 𝐴 ⊆ ( 𝐴 𝐵 ) )
29 1 28 mpan ( 𝐵C𝐴 ⊆ ( 𝐴 𝐵 ) )
30 29 adantr ( ( 𝐵C𝑥C ) → 𝐴 ⊆ ( 𝐴 𝐵 ) )
31 1 3 mpan ( 𝐵C → ( 𝐴 𝐵 ) ∈ C )
32 chlub ( ( 𝐴C𝑥C ∧ ( 𝐴 𝐵 ) ∈ C ) → ( ( 𝐴 ⊆ ( 𝐴 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) ↔ ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) ) )
33 1 32 mp3an1 ( ( 𝑥C ∧ ( 𝐴 𝐵 ) ∈ C ) → ( ( 𝐴 ⊆ ( 𝐴 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) ↔ ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) ) )
34 31 33 sylan2 ( ( 𝑥C𝐵C ) → ( ( 𝐴 ⊆ ( 𝐴 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) ↔ ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) ) )
35 34 biimpd ( ( 𝑥C𝐵C ) → ( ( 𝐴 ⊆ ( 𝐴 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) → ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) ) )
36 35 ancoms ( ( 𝐵C𝑥C ) → ( ( 𝐴 ⊆ ( 𝐴 𝐵 ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) → ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) ) )
37 30 36 mpand ( ( 𝐵C𝑥C ) → ( 𝑥 ⊆ ( 𝐴 𝐵 ) → ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) ) )
38 2 10 37 syl2an ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ⊆ ( 𝐴 𝐵 ) → ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) ) )
39 38 imp ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ 𝑥 ⊆ ( 𝐴 𝐵 ) ) → ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) )
40 27 39 sylan2 ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) )
41 40 adantrr ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( 𝐴 𝑥 ) ⊆ ( 𝐴 𝐵 ) )
42 chjcl ( ( 𝐴C𝑥C ) → ( 𝐴 𝑥 ) ∈ C )
43 1 10 42 sylancr ( 𝑥 ∈ HAtoms → ( 𝐴 𝑥 ) ∈ C )
44 2 43 anim12i ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → ( 𝐵C ∧ ( 𝐴 𝑥 ) ∈ C ) )
45 44 adantr ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( 𝐵C ∧ ( 𝐴 𝑥 ) ∈ C ) )
46 chub1 ( ( 𝐴C𝑥C ) → 𝐴 ⊆ ( 𝐴 𝑥 ) )
47 1 10 46 sylancr ( 𝑥 ∈ HAtoms → 𝐴 ⊆ ( 𝐴 𝑥 ) )
48 47 ad2antlr ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → 𝐴 ⊆ ( 𝐴 𝑥 ) )
49 pm3.22 ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) → ( 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) )
50 49 adantr ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) )
51 27 adantl ( ( 𝑥 ∈ HAtoms ∧ 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) → 𝑥 ⊆ ( 𝐴 𝐵 ) )
52 incom ( 𝐴𝑥 ) = ( 𝑥𝐴 )
53 chsh ( 𝑥C𝑥S )
54 1 chshii 𝐴S
55 orthin ( ( 𝑥S𝐴S ) → ( 𝑥 ⊆ ( ⊥ ‘ 𝐴 ) → ( 𝑥𝐴 ) = 0 ) )
56 53 54 55 sylancl ( 𝑥C → ( 𝑥 ⊆ ( ⊥ ‘ 𝐴 ) → ( 𝑥𝐴 ) = 0 ) )
57 56 imp ( ( 𝑥C𝑥 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥𝐴 ) = 0 )
58 52 57 syl5eq ( ( 𝑥C𝑥 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝐴𝑥 ) = 0 )
59 10 13 58 syl2an ( ( 𝑥 ∈ HAtoms ∧ 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝐴𝑥 ) = 0 )
60 51 59 jca ( ( 𝑥 ∈ HAtoms ∧ 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑥 ⊆ ( 𝐴 𝐵 ) ∧ ( 𝐴𝑥 ) = 0 ) )
61 60 ad2ant2lr ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( 𝑥 ⊆ ( 𝐴 𝐵 ) ∧ ( 𝐴𝑥 ) = 0 ) )
62 atexch ( ( 𝐴C𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝑥 ⊆ ( 𝐴 𝐵 ) ∧ ( 𝐴𝑥 ) = 0 ) → 𝐵 ⊆ ( 𝐴 𝑥 ) ) )
63 1 62 mp3an1 ( ( 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝑥 ⊆ ( 𝐴 𝐵 ) ∧ ( 𝐴𝑥 ) = 0 ) → 𝐵 ⊆ ( 𝐴 𝑥 ) ) )
64 50 61 63 sylc ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → 𝐵 ⊆ ( 𝐴 𝑥 ) )
65 chlub ( ( 𝐴C𝐵C ∧ ( 𝐴 𝑥 ) ∈ C ) → ( ( 𝐴 ⊆ ( 𝐴 𝑥 ) ∧ 𝐵 ⊆ ( 𝐴 𝑥 ) ) ↔ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝑥 ) ) )
66 1 65 mp3an1 ( ( 𝐵C ∧ ( 𝐴 𝑥 ) ∈ C ) → ( ( 𝐴 ⊆ ( 𝐴 𝑥 ) ∧ 𝐵 ⊆ ( 𝐴 𝑥 ) ) ↔ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝑥 ) ) )
67 66 biimpd ( ( 𝐵C ∧ ( 𝐴 𝑥 ) ∈ C ) → ( ( 𝐴 ⊆ ( 𝐴 𝑥 ) ∧ 𝐵 ⊆ ( 𝐴 𝑥 ) ) → ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝑥 ) ) )
68 67 expd ( ( 𝐵C ∧ ( 𝐴 𝑥 ) ∈ C ) → ( 𝐴 ⊆ ( 𝐴 𝑥 ) → ( 𝐵 ⊆ ( 𝐴 𝑥 ) → ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝑥 ) ) ) )
69 45 48 64 68 syl3c ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝑥 ) )
70 41 69 eqssd ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( 𝐴 𝑥 ) = ( 𝐴 𝐵 ) )
71 70 ineq1d ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( ( 𝐴 𝑥 ) ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) )
72 24 71 eqtr3d ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → 𝑥 = ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) )
73 72 eleq1d ( ( ( 𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ) ∧ ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ) → ( 𝑥 ∈ HAtoms ↔ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
74 73 exp43 ( 𝐵 ∈ HAtoms → ( 𝑥 ∈ HAtoms → ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) → ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 → ( 𝑥 ∈ HAtoms ↔ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) ) ) )
75 74 com24 ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 → ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥 ∈ HAtoms → ( 𝑥 ∈ HAtoms ↔ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) ) ) )
76 75 imp31 ( ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑥 ∈ HAtoms → ( 𝑥 ∈ HAtoms ↔ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) )
77 76 ibd ( ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑥 ∈ HAtoms → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
78 77 ex ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) → ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥 ∈ HAtoms → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) )
79 78 com23 ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) → ( 𝑥 ∈ HAtoms → ( 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) )
80 79 rexlimdv ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) → ( ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
81 9 80 mpd ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 ) → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms )
82 81 ex ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ≠ 0 → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
83 82 necon1bd ( 𝐵 ∈ HAtoms → ( ¬ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) )
84 83 orrd ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) )
85 elun ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0 } ) ↔ ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0 } ) )
86 fvex ( ⊥ ‘ 𝐴 ) ∈ V
87 86 inex2 ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ V
88 87 elsn ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0 } ↔ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 )
89 88 orbi2i ( ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0 } ) ↔ ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) )
90 85 89 bitri ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0 } ) ↔ ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) )
91 84 90 sylibr ( 𝐵 ∈ HAtoms → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0 } ) )