Theorem disjnf

Description: In case x is not free in B , disjointness is not so interesting since it reduces to cases where A is a singleton. (Google Groups discussion with Peter Mazsa.) (Contributed by Thierry Arnoux, 26-Jul-2018)

	Ref	Expression
Assertion	disjnf	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐵 = ∅ ∨ ∃* 𝑥 𝑥 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		inidm	⊢ ( 𝐵 ∩ 𝐵 ) = 𝐵
2	1	eqeq1i	⊢ ( ( 𝐵 ∩ 𝐵 ) = ∅ ↔ 𝐵 = ∅ )
3	2	orbi1i	⊢ ( ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) ↔ ( 𝐵 = ∅ ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) )
4		eqidd	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐵 )
5	4	disjor	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐵 ) = ∅ ) )
6		orcom	⊢ ( ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐵 ) = ∅ ) ↔ ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ 𝑥 = 𝑦 ) )
7	6	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐵 ) = ∅ ) ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ 𝑥 = 𝑦 ) )
8		r19.32v	⊢ ( ∀ 𝑦 ∈ 𝐴 ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ 𝑥 = 𝑦 ) ↔ ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) )
9	7 8	bitri	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐵 ) = ∅ ) ↔ ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) )
10	9	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐵 ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) )
11		r19.32v	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) ↔ ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) )
12	5 10 11	3bitri	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ( ( 𝐵 ∩ 𝐵 ) = ∅ ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) )
13		moel	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 )
14	13	orbi2i	⊢ ( ( 𝐵 = ∅ ∨ ∃* 𝑥 𝑥 ∈ 𝐴 ) ↔ ( 𝐵 = ∅ ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝑦 ) )
15	3 12 14	3bitr4i	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐵 = ∅ ∨ ∃* 𝑥 𝑥 ∈ 𝐴 ) )