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

Metamath Proof Explorer

Theorem disjiund

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

Ref Expression
Hypotheses disjiund.1 ⊢ ( 𝑎 = 𝑐 → 𝐴 = 𝐶 )
disjiund.2 ⊢ ( 𝑏 = 𝑑 → 𝐶 = 𝐷 )
disjiund.3 ⊢ ( 𝑎 = 𝑐 → 𝑊 = 𝑋 )
disjiund.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷 ) → 𝑎 = 𝑐 )
Assertion disjiund ( 𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴 )

Proof

Step Hyp Ref Expression
1 disjiund.1 ⊢ ( 𝑎 = 𝑐 → 𝐴 = 𝐶 )
2 disjiund.2 ⊢ ( 𝑏 = 𝑑 → 𝐶 = 𝐷 )
3 disjiund.3 ⊢ ( 𝑎 = 𝑐 → 𝑊 = 𝑋 )
4 disjiund.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷 ) → 𝑎 = 𝑐 )
5 eliun ⊢ ( 𝑥 ∈ ∪ 𝑏 ∈ 𝑊 𝐴 ↔ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 )
6 eliun ⊢ ( 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 ↔ ∃ 𝑏 ∈ 𝑋 𝑥 ∈ 𝐶 )
7 2 eleq2d ⊢ ( 𝑏 = 𝑑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ 𝐷 ) )
8 7 cbvrexvw ⊢ ( ∃ 𝑏 ∈ 𝑋 𝑥 ∈ 𝐶 ↔ ∃ 𝑑 ∈ 𝑋 𝑥 ∈ 𝐷 )
9 4 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐷 → 𝑎 = 𝑐 ) ) )
10 9 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐷 → 𝑎 = 𝑐 ) ) )
11 10 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐷 → 𝑎 = 𝑐 ) )
12 11 rexlimdvw ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 ) → ( ∃ 𝑑 ∈ 𝑋 𝑥 ∈ 𝐷 → 𝑎 = 𝑐 ) )
13 8 12 biimtrid ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝑋 𝑥 ∈ 𝐶 → 𝑎 = 𝑐 ) )
14 6 13 biimtrid ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 → 𝑎 = 𝑐 ) )
15 14 con3d ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 ) → ( ¬ 𝑎 = 𝑐 → ¬ 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 ) )
16 15 impancom ⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑐 ) → ( ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 ) )
17 5 16 biimtrid ⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑐 ) → ( 𝑥 ∈ ∪ 𝑏 ∈ 𝑊 𝐴 → ¬ 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 ) )
18 17 ralrimiv ⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑐 ) → ∀ 𝑥 ∈ ∪ 𝑏 ∈ 𝑊 𝐴 ¬ 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 )
19 disj ⊢ ( ( ∪ 𝑏 ∈ 𝑊 𝐴 ∩ ∪ 𝑏 ∈ 𝑋 𝐶 ) = ∅ ↔ ∀ 𝑥 ∈ ∪ 𝑏 ∈ 𝑊 𝐴 ¬ 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 )
20 18 19 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑐 ) → ( ∪ 𝑏 ∈ 𝑊 𝐴 ∩ ∪ 𝑏 ∈ 𝑋 𝐶 ) = ∅ )
21 20 ex ⊢ ( 𝜑 → ( ¬ 𝑎 = 𝑐 → ( ∪ 𝑏 ∈ 𝑊 𝐴 ∩ ∪ 𝑏 ∈ 𝑋 𝐶 ) = ∅ ) )
22 21 orrd ⊢ ( 𝜑 → ( 𝑎 = 𝑐 ∨ ( ∪ 𝑏 ∈ 𝑊 𝐴 ∩ ∪ 𝑏 ∈ 𝑋 𝐶 ) = ∅ ) )
23 22 a1d ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( 𝑎 = 𝑐 ∨ ( ∪ 𝑏 ∈ 𝑊 𝐴 ∩ ∪ 𝑏 ∈ 𝑋 𝐶 ) = ∅ ) ) )
24 23 ralrimivv ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ 𝑉 ( 𝑎 = 𝑐 ∨ ( ∪ 𝑏 ∈ 𝑊 𝐴 ∩ ∪ 𝑏 ∈ 𝑋 𝐶 ) = ∅ ) )
25 3 1 disjiunb ⊢ ( Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴 ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ 𝑉 ( 𝑎 = 𝑐 ∨ ( ∪ 𝑏 ∈ 𝑊 𝐴 ∩ ∪ 𝑏 ∈ 𝑋 𝐶 ) = ∅ ) )
26 24 25 sylibr ⊢ ( 𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴 )