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 ⊢ a = c → A = C
disjiund.2 ⊢ b = d → C = D
disjiund.3 ⊢ a = c → W = X
disjiund.4 ⊢ φ ∧ x ∈ A ∧ x ∈ D → a = c
Assertion disjiund ⊢ φ → Disj a ∈ V ⋃ b ∈ W A

Proof

Step Hyp Ref Expression
1 disjiund.1 ⊢ a = c → A = C
2 disjiund.2 ⊢ b = d → C = D
3 disjiund.3 ⊢ a = c → W = X
4 disjiund.4 ⊢ φ ∧ x ∈ A ∧ x ∈ D → a = c
5 eliun ⊢ x ∈ ⋃ b ∈ W A ↔ ∃ b ∈ W x ∈ A
6 eliun ⊢ x ∈ ⋃ b ∈ X C ↔ ∃ b ∈ X x ∈ C
7 2 eleq2d ⊢ b = d → x ∈ C ↔ x ∈ D
8 7 cbvrexvw ⊢ ∃ b ∈ X x ∈ C ↔ ∃ d ∈ X x ∈ D
9 4 3exp ⊢ φ → x ∈ A → x ∈ D → a = c
10 9 rexlimdvw ⊢ φ → ∃ b ∈ W x ∈ A → x ∈ D → a = c
11 10 imp ⊢ φ ∧ ∃ b ∈ W x ∈ A → x ∈ D → a = c
12 11 rexlimdvw ⊢ φ ∧ ∃ b ∈ W x ∈ A → ∃ d ∈ X x ∈ D → a = c
13 8 12 biimtrid ⊢ φ ∧ ∃ b ∈ W x ∈ A → ∃ b ∈ X x ∈ C → a = c
14 6 13 biimtrid ⊢ φ ∧ ∃ b ∈ W x ∈ A → x ∈ ⋃ b ∈ X C → a = c
15 14 con3d ⊢ φ ∧ ∃ b ∈ W x ∈ A → ¬ a = c → ¬ x ∈ ⋃ b ∈ X C
16 15 impancom ⊢ φ ∧ ¬ a = c → ∃ b ∈ W x ∈ A → ¬ x ∈ ⋃ b ∈ X C
17 5 16 biimtrid ⊢ φ ∧ ¬ a = c → x ∈ ⋃ b ∈ W A → ¬ x ∈ ⋃ b ∈ X C
18 17 ralrimiv ⊢ φ ∧ ¬ a = c → ∀ x ∈ ⋃ b ∈ W A ¬ x ∈ ⋃ b ∈ X C
19 disj ⊢ ⋃ b ∈ W A ∩ ⋃ b ∈ X C = ∅ ↔ ∀ x ∈ ⋃ b ∈ W A ¬ x ∈ ⋃ b ∈ X C
20 18 19 sylibr ⊢ φ ∧ ¬ a = c → ⋃ b ∈ W A ∩ ⋃ b ∈ X C = ∅
21 20 ex ⊢ φ → ¬ a = c → ⋃ b ∈ W A ∩ ⋃ b ∈ X C = ∅
22 21 orrd ⊢ φ → a = c ∨ ⋃ b ∈ W A ∩ ⋃ b ∈ X C = ∅
23 22 a1d ⊢ φ → a ∈ V ∧ c ∈ V → a = c ∨ ⋃ b ∈ W A ∩ ⋃ b ∈ X C = ∅
24 23 ralrimivv ⊢ φ → ∀ a ∈ V ∀ c ∈ V a = c ∨ ⋃ b ∈ W A ∩ ⋃ b ∈ X C = ∅
25 3 1 disjiunb ⊢ Disj a ∈ V ⋃ b ∈ W A ↔ ∀ a ∈ V ∀ c ∈ V a = c ∨ ⋃ b ∈ W A ∩ ⋃ b ∈ X C = ∅
26 24 25 sylibr ⊢ φ → Disj a ∈ V ⋃ b ∈ W A