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

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )