Theorem iinrab2

Description: Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011)

	Ref	Expression
Assertion	iinrab2	⊢ ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		iineq1	⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = ∩ 𝑥 ∈ ∅ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
2		0iin	⊢ ∩ 𝑥 ∈ ∅ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = V
3	1 2	syl6eq	⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = V )
4	3	ineq1d	⊢ ( 𝐴 = ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = ( V ∩ 𝐵 ) )
5		incom	⊢ ( V ∩ 𝐵 ) = ( 𝐵 ∩ V )
6		inv1	⊢ ( 𝐵 ∩ V ) = 𝐵
7	5 6	eqtri	⊢ ( V ∩ 𝐵 ) = 𝐵
8	4 7	syl6eq	⊢ ( 𝐴 = ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = 𝐵 )
9		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )
10		rabid2	⊢ ( 𝐵 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )
11		ralcom	⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )
12	10 11	bitr2i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ 𝐵 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
13	9 12	sylib	⊢ ( 𝐴 = ∅ → 𝐵 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
14	8 13	eqtrd	⊢ ( 𝐴 = ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
15		iinrab	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
16	15	ineq1d	⊢ ( 𝐴 ≠ ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = ( { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ∩ 𝐵 ) )
17		ssrab2	⊢ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ⊆ 𝐵
18		dfss	⊢ ( { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ⊆ 𝐵 ↔ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } = ( { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ∩ 𝐵 ) )
19	17 18	mpbi	⊢ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } = ( { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ∩ 𝐵 )
20	16 19	syl6eqr	⊢ ( 𝐴 ≠ ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
21	14 20	pm2.61ine	⊢ ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 }