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

Metamath Proof Explorer

Theorem chrelat3

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

Ref Expression
Assertion chrelat3 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 chrelat2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )
2 dfrex2 ⊢ ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ↔ ¬ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
3 1 2 bitrdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ¬ 𝐴 ⊆ 𝐵 ↔ ¬ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )
4 3 con4bid ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )
5 iman ⊢ ( ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) ↔ ¬ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
6 5 ralbii ⊢ ( ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) ↔ ∀ 𝑥 ∈ HAtoms ¬ ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) )
7 4 6 bitr4di ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) ) )