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

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 biimtrrdi ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 → 𝑥 ⊆ 𝐴 ) )
11 10 adantld ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐴 ) → 𝑥 ⊆ 𝐴 ) )
12 ssin ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
13 12 notbii ⊢ ( ¬ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
14 chnle ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
15 4 14 mpan ⊢ ( 𝑥 ∈ Cℋ → ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
16 13 15 bitrid ⊢ ( 𝑥 ∈ 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 biimtrrdi ⊢ ( 𝑥 ∈ 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 ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )