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 
|- ( A. x e. A B e. V -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )

Proof

Step Hyp Ref Expression
1 nfra1 
 |-  F/ x A. x e. A t e. B
2 nfv 
 |-  F/ x t e. z
3 eleq2 
 |-  ( z = B -> ( t e. z <-> t e. B ) )
4 vex 
 |-  z e. _V
5 4 a1i 
 |-  ( A. x e. A t e. B -> z e. _V )
6 rspa 
 |-  ( ( A. x e. A t e. B /\ x e. A ) -> t e. B )
7 1 2 3 5 6 elabreximd 
 |-  ( ( A. x e. A t e. B /\ z e. { y | E. x e. A y = B } ) -> t e. z )
8 7 ex 
 |-  ( A. x e. A t e. B -> ( z e. { y | E. x e. A y = B } -> t e. z ) )
9 8 alrimiv 
 |-  ( A. x e. A t e. B -> A. z ( z e. { y | E. x e. A y = B } -> t e. z ) )
10 9 adantl 
 |-  ( ( A. x e. A B e. V /\ A. x e. A t e. B ) -> A. z ( z e. { y | E. x e. A y = B } -> t e. z ) )
11 nfra1 
 |-  F/ x A. x e. A B e. V
12 2 nfci 
 |-  F/_ x z
13 nfre1 
 |-  F/ x E. x e. A y = B
14 13 nfab 
 |-  F/_ x { y | E. x e. A y = B }
15 12 14 nfel 
 |-  F/ x z e. { y | E. x e. A y = B }
16 15 2 nfim 
 |-  F/ x ( z e. { y | E. x e. A y = B } -> t e. z )
17 16 nfal 
 |-  F/ x A. z ( z e. { y | E. x e. A y = B } -> t e. z )
18 11 17 nfan 
 |-  F/ x ( A. x e. A B e. V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) )
19 rspa 
 |-  ( ( A. x e. A B e. V /\ x e. A ) -> B e. V )
20 19 elexd 
 |-  ( ( A. x e. A B e. V /\ x e. A ) -> B e. _V )
21 20 adantlr 
 |-  ( ( ( A. x e. A B e. V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) /\ x e. A ) -> B e. _V )
22 simplr 
 |-  ( ( ( A. x e. A B e. V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) /\ x e. A ) -> A. z ( z e. { y | E. x e. A y = B } -> t e. z ) )
23 rspe 
 |-  ( ( x e. A /\ y = B ) -> E. x e. A y = B )
24 tbtru 
 |-  ( E. x e. A y = B <-> ( E. x e. A y = B <-> T. ) )
25 23 24 sylib 
 |-  ( ( x e. A /\ y = B ) -> ( E. x e. A y = B <-> T. ) )
26 25 ex 
 |-  ( x e. A -> ( y = B -> ( E. x e. A y = B <-> T. ) ) )
27 26 alrimiv 
 |-  ( x e. A -> A. y ( y = B -> ( E. x e. A y = B <-> T. ) ) )
28 27 adantl 
 |-  ( ( ( A. x e. A B e. V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) /\ x e. A ) -> A. y ( y = B -> ( E. x e. A y = B <-> T. ) ) )
29 elabgt 
 |-  ( ( B e. _V /\ A. y ( y = B -> ( E. x e. A y = B <-> T. ) ) ) -> ( B e. { y | E. x e. A y = B } <-> T. ) )
30 tbtru 
 |-  ( B e. { y | E. x e. A y = B } <-> ( B e. { y | E. x e. A y = B } <-> T. ) )
31 29 30 sylibr 
 |-  ( ( B e. _V /\ A. y ( y = B -> ( E. x e. A y = B <-> T. ) ) ) -> B e. { y | E. x e. A y = B } )
32 21 28 31 syl2anc 
 |-  ( ( ( A. x e. A B e. V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) /\ x e. A ) -> B e. { y | E. x e. A y = B } )
33 eleq1 
 |-  ( z = B -> ( z e. { y | E. x e. A y = B } <-> B e. { y | E. x e. A y = B } ) )
34 33 3 imbi12d 
 |-  ( z = B -> ( ( z e. { y | E. x e. A y = B } -> t e. z ) <-> ( B e. { y | E. x e. A y = B } -> t e. B ) ) )
35 34 spcgv 
 |-  ( B e. _V -> ( A. z ( z e. { y | E. x e. A y = B } -> t e. z ) -> ( B e. { y | E. x e. A y = B } -> t e. B ) ) )
36 35 imp 
 |-  ( ( B e. _V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) -> ( B e. { y | E. x e. A y = B } -> t e. B ) )
37 36 imp 
 |-  ( ( ( B e. _V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) /\ B e. { y | E. x e. A y = B } ) -> t e. B )
38 21 22 32 37 syl21anc 
 |-  ( ( ( A. x e. A B e. V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) /\ x e. A ) -> t e. B )
39 38 ex 
 |-  ( ( A. x e. A B e. V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) -> ( x e. A -> t e. B ) )
40 18 39 ralrimi 
 |-  ( ( A. x e. A B e. V /\ A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) -> A. x e. A t e. B )
41 10 40 impbida 
 |-  ( A. x e. A B e. V -> ( A. x e. A t e. B <-> A. z ( z e. { y | E. x e. A y = B } -> t e. z ) ) )
42 41 abbidv 
 |-  ( A. x e. A B e. V -> { t | A. x e. A t e. B } = { t | A. z ( z e. { y | E. x e. A y = B } -> t e. z ) } )
43 df-iin 
 |-  |^|_ x e. A B = { t | A. x e. A t e. B }
44 43 a1i 
 |-  ( A. x e. A B e. V -> |^|_ x e. A B = { t | A. x e. A t e. B } )
45 df-int 
 |-  |^| { y | E. x e. A y = B } = { t | A. z ( z e. { y | E. x e. A y = B } -> t e. z ) }
46 45 a1i 
 |-  ( A. x e. A B e. V -> |^| { y | E. x e. A y = B } = { t | A. z ( z e. { y | E. x e. A y = B } -> t e. z ) } )
47 42 44 46 3eqtr4d 
 |-  ( A. x e. A B e. V -> |^|_ x e. A B = |^| { y | E. x e. A y = B } )