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 ⊢φ→Disja∈V⋃b∈WA

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∈WA↔∃b∈Wx∈A
6 eliun ⊢x∈⋃b∈XC↔∃b∈Xx∈C
7 2 eleq2d ⊢b=d→x∈C↔x∈D
8 7 cbvrexvw ⊢∃b∈Xx∈C↔∃d∈Xx∈D
9 4 3exp ⊢φ→x∈A→x∈D→a=c
10 9 rexlimdvw ⊢φ→∃b∈Wx∈A→x∈D→a=c
11 10 imp ⊢φ∧∃b∈Wx∈A→x∈D→a=c
12 11 rexlimdvw ⊢φ∧∃b∈Wx∈A→∃d∈Xx∈D→a=c
13 8 12 biimtrid ⊢φ∧∃b∈Wx∈A→∃b∈Xx∈C→a=c
14 6 13 biimtrid ⊢φ∧∃b∈Wx∈A→x∈⋃b∈XC→a=c
15 14 con3d ⊢φ∧∃b∈Wx∈A→¬a=c→¬x∈⋃b∈XC
16 15 impancom ⊢φ∧¬a=c→∃b∈Wx∈A→¬x∈⋃b∈XC
17 5 16 biimtrid ⊢φ∧¬a=c→x∈⋃b∈WA→¬x∈⋃b∈XC
18 17 ralrimiv ⊢φ∧¬a=c→∀x∈⋃b∈WA¬x∈⋃b∈XC
19 disj ⊢⋃b∈WA∩⋃b∈XC=∅↔∀x∈⋃b∈WA¬x∈⋃b∈XC
20 18 19 sylibr ⊢φ∧¬a=c→⋃b∈WA∩⋃b∈XC=∅
21 20 ex ⊢φ→¬a=c→⋃b∈WA∩⋃b∈XC=∅
22 21 orrd ⊢φ→a=c∨⋃b∈WA∩⋃b∈XC=∅
23 22 a1d ⊢φ→a∈V∧c∈V→a=c∨⋃b∈WA∩⋃b∈XC=∅
24 23 ralrimivv ⊢φ→∀a∈V∀c∈Va=c∨⋃b∈WA∩⋃b∈XC=∅
25 3 1 disjiunb ⊢Disja∈V⋃b∈WA↔∀a∈V∀c∈Va=c∨⋃b∈WA∩⋃b∈XC=∅
26 24 25 sylibr ⊢φ→Disja∈V⋃b∈WA