Metamath Proof Explorer


Theorem chrelat2i

Description: A consequence of relative atomicity. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 𝐴C
chpssat.2 𝐵C
Assertion chrelat2i ( ¬ 𝐴𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )

Proof

Step Hyp Ref Expression
1 chpssat.1 𝐴C
2 chpssat.2 𝐵C
3 nssinpss ( ¬ 𝐴𝐵 ↔ ( 𝐴𝐵 ) ⊊ 𝐴 )
4 1 2 chincli ( 𝐴𝐵 ) ∈ C
5 4 1 chrelati ( ( 𝐴𝐵 ) ⊊ 𝐴 → ∃ 𝑥 ∈ HAtoms ( ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ∧ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) )
6 atelch ( 𝑥 ∈ HAtoms → 𝑥C )
7 chlub ( ( ( 𝐴𝐵 ) ∈ C𝑥C𝐴C ) → ( ( ( 𝐴𝐵 ) ⊆ 𝐴𝑥𝐴 ) ↔ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) )
8 4 1 7 mp3an13 ( 𝑥C → ( ( ( 𝐴𝐵 ) ⊆ 𝐴𝑥𝐴 ) ↔ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) )
9 simpr ( ( ( 𝐴𝐵 ) ⊆ 𝐴𝑥𝐴 ) → 𝑥𝐴 )
10 8 9 syl6bir ( 𝑥C → ( ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴𝑥𝐴 ) )
11 10 adantld ( 𝑥C → ( ( ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ∧ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) → 𝑥𝐴 ) )
12 ssin ( ( 𝑥𝐴𝑥𝐵 ) ↔ 𝑥 ⊆ ( 𝐴𝐵 ) )
13 12 notbii ( ¬ ( 𝑥𝐴𝑥𝐵 ) ↔ ¬ 𝑥 ⊆ ( 𝐴𝐵 ) )
14 chnle ( ( ( 𝐴𝐵 ) ∈ C𝑥C ) → ( ¬ 𝑥 ⊆ ( 𝐴𝐵 ) ↔ ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ) )
15 4 14 mpan ( 𝑥C → ( ¬ 𝑥 ⊆ ( 𝐴𝐵 ) ↔ ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ) )
16 13 15 syl5bb ( 𝑥C → ( ¬ ( 𝑥𝐴𝑥𝐵 ) ↔ ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ) )
17 16 8 anbi12d ( 𝑥C → ( ( ¬ ( 𝑥𝐴𝑥𝐵 ) ∧ ( ( 𝐴𝐵 ) ⊆ 𝐴𝑥𝐴 ) ) ↔ ( ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ∧ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) ) )
18 pm3.21 ( 𝑥𝐵 → ( 𝑥𝐴 → ( 𝑥𝐴𝑥𝐵 ) ) )
19 orcom ( ( ( 𝑥𝐴𝑥𝐵 ) ∨ ¬ 𝑥𝐴 ) ↔ ( ¬ 𝑥𝐴 ∨ ( 𝑥𝐴𝑥𝐵 ) ) )
20 pm4.55 ( ¬ ( ¬ ( 𝑥𝐴𝑥𝐵 ) ∧ 𝑥𝐴 ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∨ ¬ 𝑥𝐴 ) )
21 imor ( ( 𝑥𝐴 → ( 𝑥𝐴𝑥𝐵 ) ) ↔ ( ¬ 𝑥𝐴 ∨ ( 𝑥𝐴𝑥𝐵 ) ) )
22 19 20 21 3bitr4ri ( ( 𝑥𝐴 → ( 𝑥𝐴𝑥𝐵 ) ) ↔ ¬ ( ¬ ( 𝑥𝐴𝑥𝐵 ) ∧ 𝑥𝐴 ) )
23 18 22 sylib ( 𝑥𝐵 → ¬ ( ¬ ( 𝑥𝐴𝑥𝐵 ) ∧ 𝑥𝐴 ) )
24 23 con2i ( ( ¬ ( 𝑥𝐴𝑥𝐵 ) ∧ 𝑥𝐴 ) → ¬ 𝑥𝐵 )
25 24 adantrl ( ( ¬ ( 𝑥𝐴𝑥𝐵 ) ∧ ( ( 𝐴𝐵 ) ⊆ 𝐴𝑥𝐴 ) ) → ¬ 𝑥𝐵 )
26 17 25 syl6bir ( 𝑥C → ( ( ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ∧ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) → ¬ 𝑥𝐵 ) )
27 11 26 jcad ( 𝑥C → ( ( ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ∧ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) → ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ) )
28 6 27 syl ( 𝑥 ∈ HAtoms → ( ( ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ∧ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) → ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ) )
29 28 reximia ( ∃ 𝑥 ∈ HAtoms ( ( 𝐴𝐵 ) ⊊ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ∧ ( ( 𝐴𝐵 ) ∨ 𝑥 ) ⊆ 𝐴 ) → ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
30 5 29 syl ( ( 𝐴𝐵 ) ⊊ 𝐴 → ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
31 3 30 sylbi ( ¬ 𝐴𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
32 sstr2 ( 𝑥𝐴 → ( 𝐴𝐵𝑥𝐵 ) )
33 32 com12 ( 𝐴𝐵 → ( 𝑥𝐴𝑥𝐵 ) )
34 33 ralrimivw ( 𝐴𝐵 → ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) )
35 iman ( ( 𝑥𝐴𝑥𝐵 ) ↔ ¬ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
36 35 ralbii ( ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ↔ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
37 ralnex ( ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) ↔ ¬ ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
38 36 37 bitri ( ∀ 𝑥 ∈ HAtoms ( 𝑥𝐴𝑥𝐵 ) ↔ ¬ ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
39 34 38 sylib ( 𝐴𝐵 → ¬ ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )
40 39 con2i ( ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) → ¬ 𝐴𝐵 )
41 31 40 impbii ( ¬ 𝐴𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥𝐴 ∧ ¬ 𝑥𝐵 ) )