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

Metamath Proof Explorer

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 𝑎 ∈ 𝑉 𝐴 )