Metamath Proof Explorer

Theorem dfdfat2

Description: Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfdfat2 
|- ( F defAt A <-> ( A e. dom F /\ E! y A F y ) )

Proof

Step Hyp Ref Expression
1 df-dfat 
 |-  ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
2 relres 
 |-  Rel ( F |` { A } )
3 dffun8 
 |-  ( Fun ( F |` { A } ) <-> ( Rel ( F |` { A } ) /\ A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y ) )
4 2 3 mpbiran 
 |-  ( Fun ( F |` { A } ) <-> A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y )
5 4 anbi2i 
 |-  ( ( A e. dom F /\ Fun ( F |` { A } ) ) <-> ( A e. dom F /\ A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y ) )
6 brres 
 |-  ( y e. _V -> ( x ( F |` { A } ) y <-> ( x e. { A } /\ x F y ) ) )
7 6 elv 
 |-  ( x ( F |` { A } ) y <-> ( x e. { A } /\ x F y ) )
8 7 a1i 
 |-  ( A e. dom F -> ( x ( F |` { A } ) y <-> ( x e. { A } /\ x F y ) ) )
9 8 eubidv 
 |-  ( A e. dom F -> ( E! y x ( F |` { A } ) y <-> E! y ( x e. { A } /\ x F y ) ) )
10 9 ralbidv 
 |-  ( A e. dom F -> ( A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y <-> A. x e. dom ( F |` { A } ) E! y ( x e. { A } /\ x F y ) ) )
11 eldmressnsn 
 |-  ( A e. dom F -> A e. dom ( F |` { A } ) )
12 eldmressn 
 |-  ( x e. dom ( F |` { A } ) -> x = A )
13 velsn 
 |-  ( x e. { A } <-> x = A )
14 13 biimpri 
 |-  ( x = A -> x e. { A } )
15 breq1 
 |-  ( x = A -> ( x F y <-> A F y ) )
16 15 anbi2d 
 |-  ( x = A -> ( ( x e. { A } /\ x F y ) <-> ( x e. { A } /\ A F y ) ) )
17 14 16 mpbirand 
 |-  ( x = A -> ( ( x e. { A } /\ x F y ) <-> A F y ) )
18 17 eubidv 
 |-  ( x = A -> ( E! y ( x e. { A } /\ x F y ) <-> E! y A F y ) )
19 11 12 18 ralbinrald 
 |-  ( A e. dom F -> ( A. x e. dom ( F |` { A } ) E! y ( x e. { A } /\ x F y ) <-> E! y A F y ) )
20 10 19 bitrd 
 |-  ( A e. dom F -> ( A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y <-> E! y A F y ) )
21 20 pm5.32i 
 |-  ( ( A e. dom F /\ A. x e. dom ( F |` { A } ) E! y x ( F |` { A } ) y ) <-> ( A e. dom F /\ E! y A F y ) )
22 1 5 21 3bitri 
 |-  ( F defAt A <-> ( A e. dom F /\ E! y A F y ) )