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ℋ } ) )