Theorem dfiin2g

Description: Alternate definition of indexed intersection when B is a set. (Contributed by Jeff Hankins, 27-Aug-2009)

	Ref	Expression
Assertion	dfiin2g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) )
3		clel4g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
4	3	imim2i	⊢ ( ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
5	4	pm5.74d	⊢ ( ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
6	5	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
7		albi	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
8	6 7	syl	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
9	2 8	sylbi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
10		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
11	10	albii	⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
12		alcom	⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
13	11 12	bitr4i	⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
14		r19.23v	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) )
15		vex	⊢ 𝑧 ∈ V
16		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑧 = 𝐵 ) )
17	16	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
18	15 17	elab	⊢ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
19	18	imbi1i	⊢ ( ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) )
20	14 19	bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
21	20	albii	⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
22		19.21v	⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
23	22	albii	⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
24	13 21 23	3bitr3ri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
25	9 24	bitrdi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ) )
26	1 25	bitrid	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ) )
27	26	abbidv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → { 𝑤 ∣ ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 } = { 𝑤 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) } )
28		df-iin	⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑤 ∣ ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 }
29		df-int	⊢ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = { 𝑤 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) }
30	27 28 29	3eqtr4g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )