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 ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) ) )