Metamath Proof Explorer

Theorem fineqvrep

Description: If the Axiom of Infinity is negated, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024)

Ref Expression
Assertion fineqvrep 
|- ( Fin = _V -> ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) )

Proof

Step Hyp Ref Expression
1 funopab 
 |-  ( Fun { <. w , z >. | A. y ph } <-> A. w E* z A. y ph )
2 nfa1 
 |-  F/ y A. y ph
3 2 mof 
 |-  ( E* z A. y ph <-> E. y A. z ( A. y ph -> z = y ) )
4 3 albii 
 |-  ( A. w E* z A. y ph <-> A. w E. y A. z ( A. y ph -> z = y ) )
5 1 4 bitr2i 
 |-  ( A. w E. y A. z ( A. y ph -> z = y ) <-> Fun { <. w , z >. | A. y ph } )
6 vex 
 |-  x e. _V
7 eleq2w2 
 |-  ( Fin = _V -> ( x e. Fin <-> x e. _V ) )
8 6 7 mpbiri 
 |-  ( Fin = _V -> x e. Fin )
9 imafi 
 |-  ( ( Fun { <. w , z >. | A. y ph } /\ x e. Fin ) -> ( { <. w , z >. | A. y ph } " x ) e. Fin )
10 8 9 sylan2 
 |-  ( ( Fun { <. w , z >. | A. y ph } /\ Fin = _V ) -> ( { <. w , z >. | A. y ph } " x ) e. Fin )
11 10 elexd 
 |-  ( ( Fun { <. w , z >. | A. y ph } /\ Fin = _V ) -> ( { <. w , z >. | A. y ph } " x ) e. _V )
12 nfv 
 |-  F/ y w e. x
13 2 nfopab 
 |-  F/_ y { <. w , z >. | A. y ph }
14 13 nfel2 
 |-  F/ y <. w , z >. e. { <. w , z >. | A. y ph }
15 12 14 nfan 
 |-  F/ y ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } )
16 15 nfex 
 |-  F/ y E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } )
17 16 nfab 
 |-  F/_ y { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) }
18 17 issetf 
 |-  ( { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) } e. _V <-> E. y y = { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) } )
19 abeq2 
 |-  ( y = { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) } <-> A. z ( z e. y <-> E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) ) )
20 19 exbii 
 |-  ( E. y y = { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) } <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) ) )
21 opabidw 
 |-  ( <. w , z >. e. { <. w , z >. | A. y ph } <-> A. y ph )
22 21 anbi2i 
 |-  ( ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) <-> ( w e. x /\ A. y ph ) )
23 22 exbii 
 |-  ( E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) <-> E. w ( w e. x /\ A. y ph ) )
24 23 bibi2i 
 |-  ( ( z e. y <-> E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) ) <-> ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
25 24 albii 
 |-  ( A. z ( z e. y <-> E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) ) <-> A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
26 25 exbii 
 |-  ( E. y A. z ( z e. y <-> E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) ) <-> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
27 18 20 26 3bitrri 
 |-  ( E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) <-> { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) } e. _V )
28 dfima3 
 |-  ( { <. w , z >. | A. y ph } " x ) = { v | E. u ( u e. x /\ <. u , v >. e. { <. w , z >. | A. y ph } ) }
29 nfv 
 |-  F/ z u e. x
30 nfopab2 
 |-  F/_ z { <. w , z >. | A. y ph }
31 30 nfel2 
 |-  F/ z <. u , v >. e. { <. w , z >. | A. y ph }
32 29 31 nfan 
 |-  F/ z ( u e. x /\ <. u , v >. e. { <. w , z >. | A. y ph } )
33 32 nfex 
 |-  F/ z E. u ( u e. x /\ <. u , v >. e. { <. w , z >. | A. y ph } )
34 nfv 
 |-  F/ v E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } )
35 nfv 
 |-  F/ w u e. x
36 nfopab1 
 |-  F/_ w { <. w , z >. | A. y ph }
37 36 nfel2 
 |-  F/ w <. u , v >. e. { <. w , z >. | A. y ph }
38 35 37 nfan 
 |-  F/ w ( u e. x /\ <. u , v >. e. { <. w , z >. | A. y ph } )
39 nfv 
 |-  F/ u ( w e. x /\ <. w , v >. e. { <. w , z >. | A. y ph } )
40 elequ1 
 |-  ( u = w -> ( u e. x <-> w e. x ) )
41 opeq1 
 |-  ( u = w -> <. u , v >. = <. w , v >. )
42 41 eleq1d 
 |-  ( u = w -> ( <. u , v >. e. { <. w , z >. | A. y ph } <-> <. w , v >. e. { <. w , z >. | A. y ph } ) )
43 40 42 anbi12d 
 |-  ( u = w -> ( ( u e. x /\ <. u , v >. e. { <. w , z >. | A. y ph } ) <-> ( w e. x /\ <. w , v >. e. { <. w , z >. | A. y ph } ) ) )
44 38 39 43 cbvexv1 
 |-  ( E. u ( u e. x /\ <. u , v >. e. { <. w , z >. | A. y ph } ) <-> E. w ( w e. x /\ <. w , v >. e. { <. w , z >. | A. y ph } ) )
45 opeq2 
 |-  ( v = z -> <. w , v >. = <. w , z >. )
46 45 eleq1d 
 |-  ( v = z -> ( <. w , v >. e. { <. w , z >. | A. y ph } <-> <. w , z >. e. { <. w , z >. | A. y ph } ) )
47 46 anbi2d 
 |-  ( v = z -> ( ( w e. x /\ <. w , v >. e. { <. w , z >. | A. y ph } ) <-> ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) ) )
48 47 exbidv 
 |-  ( v = z -> ( E. w ( w e. x /\ <. w , v >. e. { <. w , z >. | A. y ph } ) <-> E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) ) )
49 44 48 syl5bb 
 |-  ( v = z -> ( E. u ( u e. x /\ <. u , v >. e. { <. w , z >. | A. y ph } ) <-> E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) ) )
50 33 34 49 cbvabw 
 |-  { v | E. u ( u e. x /\ <. u , v >. e. { <. w , z >. | A. y ph } ) } = { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) }
51 28 50 eqtri 
 |-  ( { <. w , z >. | A. y ph } " x ) = { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) }
52 51 eleq1i 
 |-  ( ( { <. w , z >. | A. y ph } " x ) e. _V <-> { z | E. w ( w e. x /\ <. w , z >. e. { <. w , z >. | A. y ph } ) } e. _V )
53 27 52 bitr4i 
 |-  ( E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) <-> ( { <. w , z >. | A. y ph } " x ) e. _V )
54 11 53 sylibr 
 |-  ( ( Fun { <. w , z >. | A. y ph } /\ Fin = _V ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
55 5 54 sylanb 
 |-  ( ( A. w E. y A. z ( A. y ph -> z = y ) /\ Fin = _V ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
56 55 expcom 
 |-  ( Fin = _V -> ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) )