Theorem disjord

Description: Conditions for a collection of sets A ( a ) for a e. V to be disjoint. (Contributed by AV, 9-Jan-2022)

	Ref	Expression
Hypotheses	disjord.1	⊢ ( 𝑎 = 𝑏 → 𝐴 = 𝐵 )
	disjord.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑎 = 𝑏 )
Assertion	disjord	⊢ ( 𝜑 → Disj 𝑎 ∈ 𝑉 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		disjord.1	⊢ ( 𝑎 = 𝑏 → 𝐴 = 𝐵 )
2		disjord.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑎 = 𝑏 )
3		orc	⊢ ( 𝑎 = 𝑏 → ( 𝑎 = 𝑏 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
4	3	a1d	⊢ ( 𝑎 = 𝑏 → ( 𝜑 → ( 𝑎 = 𝑏 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
5	2	3expia	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 → 𝑎 = 𝑏 ) )
6	5	con3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑎 = 𝑏 → ¬ 𝑥 ∈ 𝐵 ) )
7	6	impancom	⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑏 ) → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵 ) )
8	7	ralrimiv	⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑏 ) → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )
9		disj	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )
10	8 9	sylibr	⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑏 ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
11	10	olcd	⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑏 ) → ( 𝑎 = 𝑏 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
12	11	expcom	⊢ ( ¬ 𝑎 = 𝑏 → ( 𝜑 → ( 𝑎 = 𝑏 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
13	4 12	pm2.61i	⊢ ( 𝜑 → ( 𝑎 = 𝑏 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 = 𝑏 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
15	14	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑎 = 𝑏 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
16	1	disjor	⊢ ( Disj 𝑎 ∈ 𝑉 𝐴 ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑎 = 𝑏 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
17	15 16	sylibr	⊢ ( 𝜑 → Disj 𝑎 ∈ 𝑉 𝐴 )