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 ⊢ a = b → A = B
disjord.2 ⊢ φ ∧ x ∈ A ∧ x ∈ B → a = b
Assertion disjord ⊢ φ → Disj a ∈ V A

Proof

Step Hyp Ref Expression
1 disjord.1 ⊢ a = b → A = B
2 disjord.2 ⊢ φ ∧ x ∈ A ∧ x ∈ B → a = b
3 orc ⊢ a = b → a = b ∨ A ∩ B = ∅
4 3 a1d ⊢ a = b → φ → a = b ∨ A ∩ B = ∅
5 2 3expia ⊢ φ ∧ x ∈ A → x ∈ B → a = b
6 5 con3d ⊢ φ ∧ x ∈ A → ¬ a = b → ¬ x ∈ B
7 6 impancom ⊢ φ ∧ ¬ a = b → x ∈ A → ¬ x ∈ B
8 7 ralrimiv ⊢ φ ∧ ¬ a = b → ∀ x ∈ A ¬ x ∈ B
9 disj ⊢ A ∩ B = ∅ ↔ ∀ x ∈ A ¬ x ∈ B
10 8 9 sylibr ⊢ φ ∧ ¬ a = b → A ∩ B = ∅
11 10 olcd ⊢ φ ∧ ¬ a = b → a = b ∨ A ∩ B = ∅
12 11 expcom ⊢ ¬ a = b → φ → a = b ∨ A ∩ B = ∅
13 4 12 pm2.61i ⊢ φ → a = b ∨ A ∩ B = ∅
14 13 adantr ⊢ φ ∧ a ∈ V ∧ b ∈ V → a = b ∨ A ∩ B = ∅
15 14 ralrimivva ⊢ φ → ∀ a ∈ V ∀ b ∈ V a = b ∨ A ∩ B = ∅
16 1 disjor ⊢ Disj a ∈ V A ↔ ∀ a ∈ V ∀ b ∈ V a = b ∨ A ∩ B = ∅
17 15 16 sylibr ⊢ φ → Disj a ∈ V A