Metamath Proof Explorer

Theorem tz6.12-afv2

Description: Function value (Theorem 6.12(1) of TakeutiZaring p. 27), analogous to tz6.12 . (Contributed by AV, 5-Sep-2022)

Ref Expression
Assertion tz6.12-afv2 
|- ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F '''' A ) = y )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. _V /\ <. A , y >. e. F ) -> A e. _V )
2 vex 
 |-  y e. _V
3 2 a1i 
 |-  ( ( A e. _V /\ <. A , y >. e. F ) -> y e. _V )
4 df-br 
 |-  ( A F y <-> <. A , y >. e. F )
5 4 biimpri 
 |-  ( <. A , y >. e. F -> A F y )
6 5 adantl 
 |-  ( ( A e. _V /\ <. A , y >. e. F ) -> A F y )
7 breldmg 
 |-  ( ( A e. _V /\ y e. _V /\ A F y ) -> A e. dom F )
8 1 3 6 7 syl3anc 
 |-  ( ( A e. _V /\ <. A , y >. e. F ) -> A e. dom F )
9 simpl 
 |-  ( ( A e. dom F /\ E! y <. A , y >. e. F ) -> A e. dom F )
10 velsn 
 |-  ( x e. { A } <-> x = A )
11 breq1 
 |-  ( A = x -> ( A F y <-> x F y ) )
12 4 11 bitr3id 
 |-  ( A = x -> ( <. A , y >. e. F <-> x F y ) )
13 12 eqcoms 
 |-  ( x = A -> ( <. A , y >. e. F <-> x F y ) )
14 13 eubidv 
 |-  ( x = A -> ( E! y <. A , y >. e. F <-> E! y x F y ) )
15 14 biimpd 
 |-  ( x = A -> ( E! y <. A , y >. e. F -> E! y x F y ) )
16 10 15 sylbi 
 |-  ( x e. { A } -> ( E! y <. A , y >. e. F -> E! y x F y ) )
17 16 com12 
 |-  ( E! y <. A , y >. e. F -> ( x e. { A } -> E! y x F y ) )
18 17 adantl 
 |-  ( ( A e. dom F /\ E! y <. A , y >. e. F ) -> ( x e. { A } -> E! y x F y ) )
19 18 ralrimiv 
 |-  ( ( A e. dom F /\ E! y <. A , y >. e. F ) -> A. x e. { A } E! y x F y )
20 fnres 
 |-  ( ( F |` { A } ) Fn { A } <-> A. x e. { A } E! y x F y )
21 fnfun 
 |-  ( ( F |` { A } ) Fn { A } -> Fun ( F |` { A } ) )
22 20 21 sylbir 
 |-  ( A. x e. { A } E! y x F y -> Fun ( F |` { A } ) )
23 19 22 syl 
 |-  ( ( A e. dom F /\ E! y <. A , y >. e. F ) -> Fun ( F |` { A } ) )
24 9 23 jca 
 |-  ( ( A e. dom F /\ E! y <. A , y >. e. F ) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )
25 24 ex 
 |-  ( A e. dom F -> ( E! y <. A , y >. e. F -> ( A e. dom F /\ Fun ( F |` { A } ) ) ) )
26 8 25 syl 
 |-  ( ( A e. _V /\ <. A , y >. e. F ) -> ( E! y <. A , y >. e. F -> ( A e. dom F /\ Fun ( F |` { A } ) ) ) )
27 26 impr 
 |-  ( ( A e. _V /\ ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) ) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )
28 df-dfat 
 |-  ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
29 27 28 sylibr 
 |-  ( ( A e. _V /\ ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) ) -> F defAt A )
30 dfatafv2iota 
 |-  ( F defAt A -> ( F '''' A ) = ( iota y A F y ) )
31 29 30 syl 
 |-  ( ( A e. _V /\ ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) ) -> ( F '''' A ) = ( iota y A F y ) )
32 4 bicomi 
 |-  ( <. A , y >. e. F <-> A F y )
33 32 eubii 
 |-  ( E! y <. A , y >. e. F <-> E! y A F y )
34 33 biimpi 
 |-  ( E! y <. A , y >. e. F -> E! y A F y )
35 5 34 anim12i 
 |-  ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( A F y /\ E! y A F y ) )
36 35 adantl 
 |-  ( ( A e. _V /\ ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) ) -> ( A F y /\ E! y A F y ) )
37 iota1 
 |-  ( E! y A F y -> ( A F y <-> ( iota y A F y ) = y ) )
38 37 biimpac 
 |-  ( ( A F y /\ E! y A F y ) -> ( iota y A F y ) = y )
39 36 38 syl 
 |-  ( ( A e. _V /\ ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) ) -> ( iota y A F y ) = y )
40 31 39 eqtrd 
 |-  ( ( A e. _V /\ ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) ) -> ( F '''' A ) = y )
41 40 ex 
 |-  ( A e. _V -> ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F '''' A ) = y ) )
42 eu2ndop1stv 
 |-  ( E! y <. A , y >. e. F -> A e. _V )
43 42 pm2.24d 
 |-  ( E! y <. A , y >. e. F -> ( -. A e. _V -> ( F '''' A ) = y ) )
44 43 adantl 
 |-  ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( -. A e. _V -> ( F '''' A ) = y ) )
45 44 com12 
 |-  ( -. A e. _V -> ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F '''' A ) = y ) )
46 41 45 pm2.61i 
 |-  ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F '''' A ) = y )