Theorem iuniin

Description: Law combining indexed union with indexed intersection. Eq. 14 in KuratowskiMostowski p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29 . (Contributed by NM, 17-Aug-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	iuniin	⊢ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ⊆ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶

Proof

Step	Hyp	Ref	Expression
1		r19.12	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
2		eliin	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 ) )
3	2	elv	⊢ ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
4	3	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
5		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
6	5	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
7	1 4 6	3imtr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 → ∀ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 )
8		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 )
9		eliin	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
10	9	elv	⊢ ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 )
11	7 8 10	3imtr4i	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 → 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 )
12	11	ssriv	⊢ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ⊆ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶