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

Metamath Proof Explorer

Theorem iinuni

Description: A relationship involving union and indexed intersection. Exercise 23 of Enderton p. 33. (Contributed by NM, 25-Nov-2003) (Proof shortened by Mario Carneiro, 17-Nov-2016)

		Ref	Expression
	Assertion	iinuni	⊢ ( 𝐴 ∪ ∩ 𝐵 ) = ∩ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		r19.32v	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 ∨ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ) )
2		elun	⊢ ( 𝑦 ∈ ( 𝐴 ∪ 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝑥 ) )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ∪ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝑥 ) )
4		vex	⊢ 𝑦 ∈ V
5	4	elint2	⊢ ( 𝑦 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 )
6	5	orbi2i	⊢ ( ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ ∩ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∨ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ) )
7	1 3 6	3bitr4ri	⊢ ( ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ ∩ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ∪ 𝑥 ) )
8	7	abbii	⊢ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ ∩ 𝐵 ) } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ∪ 𝑥 ) }
9		df-un	⊢ ( 𝐴 ∪ ∩ 𝐵 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ ∩ 𝐵 ) }
10		df-iin	⊢ ∩ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 ∪ 𝑥 ) }
11	8 9 10	3eqtr4i	⊢ ( 𝐴 ∪ ∩ 𝐵 ) = ∩ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 )