Theorem iinabrex

Description: Rewriting an indexed intersection into an intersection of its image set. (Contributed by Thierry Arnoux, 15-Jun-2024)

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

Proof

Step	Hyp	Ref	Expression
1		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵
2		nfv	⊢ Ⅎ 𝑥 𝑡 ∈ 𝑧
3		eleq2	⊢ ( 𝑧 = 𝐵 → ( 𝑡 ∈ 𝑧 ↔ 𝑡 ∈ 𝐵 ) )
4		vex	⊢ 𝑧 ∈ V
5	4	a1i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 → 𝑧 ∈ V )
6		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑡 ∈ 𝐵 )
7	1 2 3 5 6	elabreximd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) → 𝑡 ∈ 𝑧 )
8	7	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 → ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) )
9	8	alrimiv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 → ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) )
10	9	adantl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 ) → ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) )
11		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉
12	2	nfci	⊢ Ⅎ 𝑥 𝑧
13		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵
14	13	nfab	⊢ Ⅎ 𝑥 { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
15	12 14	nfel	⊢ Ⅎ 𝑥 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
16	15 2	nfim	⊢ Ⅎ 𝑥 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 )
17	16	nfal	⊢ Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 )
18	11 17	nfan	⊢ Ⅎ 𝑥 ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) )
19		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
20	19	elexd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ V )
21	20	adantlr	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ V )
22		simplr	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) )
23		rspe	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
24		tbtru	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤ ) )
25	23 24	sylib	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤ ) )
26	25	ex	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤ ) ) )
27	26	alrimiv	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤ ) ) )
28	27	adantl	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤ ) ) )
29		elabgt	⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤ ) ) ) → ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ⊤ ) )
30		tbtru	⊢ ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ⊤ ) )
31	29 30	sylibr	⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑦 ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ⊤ ) ) ) → 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
32	21 28 31	syl2anc	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
33		eleq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) )
34	33 3	imbi12d	⊢ ( 𝑧 = 𝐵 → ( ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ↔ ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝐵 ) ) )
35	34	spcgv	⊢ ( 𝐵 ∈ V → ( ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) → ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝐵 ) ) )
36	35	imp	⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) → ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝐵 ) )
37	36	imp	⊢ ( ( ( 𝐵 ∈ V ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) ∧ 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) → 𝑡 ∈ 𝐵 )
38	21 22 32 37	syl21anc	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑡 ∈ 𝐵 )
39	38	ex	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) → ( 𝑥 ∈ 𝐴 → 𝑡 ∈ 𝐵 ) )
40	18 39	ralrimi	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) → ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 )
41	10 40	impbida	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) ) )
42	41	abbidv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → { 𝑡 ∣ ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 } = { 𝑡 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) } )
43		df-iin	⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑡 ∣ ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 }
44	43	a1i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑡 ∣ ∀ 𝑥 ∈ 𝐴 𝑡 ∈ 𝐵 } )
45		df-int	⊢ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = { 𝑡 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) }
46	45	a1i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = { 𝑡 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑡 ∈ 𝑧 ) } )
47	42 44 46	3eqtr4d	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )