Metamath Proof Explorer

Theorem chrelat2

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

		Ref	Expression
	Assertion	chrelat2	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseq1	⊢ ( 𝐴 = if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) → ( 𝐴 ⊆ 𝐵 ↔ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ 𝐵 ) )
2	1	notbid	⊢ ( 𝐴 = if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) → ( ¬ 𝐴 ⊆ 𝐵 ↔ ¬ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ 𝐵 ) )
3		sseq2	⊢ ( 𝐴 = if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ) )
4	3	anbi1d	⊢ ( 𝐴 = if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) → ( ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ↔ ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )
5	4	rexbidv	⊢ ( 𝐴 = if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) → ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )
6	2 5	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) → ( ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) ↔ ( ¬ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ 𝐵 ) ) ) )
7		sseq2	⊢ ( 𝐵 = if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) → ( if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ 𝐵 ↔ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ) )
8	7	notbid	⊢ ( 𝐵 = if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) → ( ¬ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ 𝐵 ↔ ¬ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ) )
9		sseq2	⊢ ( 𝐵 = if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) → ( 𝑥 ⊆ 𝐵 ↔ 𝑥 ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ) )
10	9	notbid	⊢ ( 𝐵 = if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) → ( ¬ 𝑥 ⊆ 𝐵 ↔ ¬ 𝑥 ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ) )
11	10	anbi2d	⊢ ( 𝐵 = if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) → ( ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ 𝐵 ) ↔ ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ) ) )
12	11	rexbidv	⊢ ( 𝐵 = if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) → ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ 𝐵 ) ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ) ) )
13	8 12	bibi12d	⊢ ( 𝐵 = if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) → ( ( ¬ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ 𝐵 ) ) ↔ ( ¬ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ) ) ) )
14		ifchhv	⊢ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∈ C_ℋ
15		ifchhv	⊢ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ∈ C_ℋ
16	14 15	chrelat2i	⊢ ( ¬ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ if ( 𝐴 ∈ C_ℋ , 𝐴 , ℋ ) ∧ ¬ 𝑥 ⊆ if ( 𝐵 ∈ C_ℋ , 𝐵 , ℋ ) ) )
17	6 13 16	dedth2h	⊢ ( ( 𝐴 ∈ C_ℋ ∧ 𝐵 ∈ C_ℋ ) → ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵 ) ) )