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	syl5bi	⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝑋 𝑥 ∈ 𝐶 → 𝑎 = 𝑐 ) )
14	6 13	syl5bi	⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 → 𝑎 = 𝑐 ) )
15	14	con3d	⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 ) → ( ¬ 𝑎 = 𝑐 → ¬ 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 ) )
16	15	impancom	⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑐 ) → ( ∃ 𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 ) )
17	5 16	syl5bi	⊢ ( ( 𝜑 ∧ ¬ 𝑎 = 𝑐 ) → ( 𝑥 ∈ ∪ 𝑏 ∈ 𝑊 𝐴 → ¬ 𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 ) )
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 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴 )