Metamath Proof Explorer

Theorem dfatcolem

Description: Lemma for dfatco . (Contributed by AV, 8-Sep-2022)

Ref Expression
Assertion dfatcolem 
|- ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E! y X ( F o. G ) y )

Proof

Step Hyp Ref Expression
1 dfdfat2 
 |-  ( F defAt ( G '''' X ) <-> ( ( G '''' X ) e. dom F /\ E! y ( G '''' X ) F y ) )
2 eqidd 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( G '''' X ) = ( G '''' X ) )
3 df-dfat 
 |-  ( F defAt ( G '''' X ) <-> ( ( G '''' X ) e. dom F /\ Fun ( F |` { ( G '''' X ) } ) ) )
4 3 simplbi 
 |-  ( F defAt ( G '''' X ) -> ( G '''' X ) e. dom F )
5 dfatbrafv2b 
 |-  ( ( G defAt X /\ ( G '''' X ) e. dom F ) -> ( ( G '''' X ) = ( G '''' X ) <-> X G ( G '''' X ) ) )
6 4 5 sylan2 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( G '''' X ) = ( G '''' X ) <-> X G ( G '''' X ) ) )
7 2 6 mpbid 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> X G ( G '''' X ) )
8 eqidd 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( F '''' ( G '''' X ) ) = ( F '''' ( G '''' X ) ) )
9 simpr 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> F defAt ( G '''' X ) )
10 dfatafv2ex 
 |-  ( F defAt ( G '''' X ) -> ( F '''' ( G '''' X ) ) e. _V )
11 10 adantl 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( F '''' ( G '''' X ) ) e. _V )
12 dfatbrafv2b 
 |-  ( ( F defAt ( G '''' X ) /\ ( F '''' ( G '''' X ) ) e. _V ) -> ( ( F '''' ( G '''' X ) ) = ( F '''' ( G '''' X ) ) <-> ( G '''' X ) F ( F '''' ( G '''' X ) ) ) )
13 9 11 12 syl2anc 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( F '''' ( G '''' X ) ) = ( F '''' ( G '''' X ) ) <-> ( G '''' X ) F ( F '''' ( G '''' X ) ) ) )
14 8 13 mpbid 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( G '''' X ) F ( F '''' ( G '''' X ) ) )
15 4 adantl 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( G '''' X ) e. dom F )
16 breq2 
 |-  ( z = ( G '''' X ) -> ( X G z <-> X G ( G '''' X ) ) )
17 16 adantl 
 |-  ( ( y = ( F '''' ( G '''' X ) ) /\ z = ( G '''' X ) ) -> ( X G z <-> X G ( G '''' X ) ) )
18 breq12 
 |-  ( ( z = ( G '''' X ) /\ y = ( F '''' ( G '''' X ) ) ) -> ( z F y <-> ( G '''' X ) F ( F '''' ( G '''' X ) ) ) )
19 18 ancoms 
 |-  ( ( y = ( F '''' ( G '''' X ) ) /\ z = ( G '''' X ) ) -> ( z F y <-> ( G '''' X ) F ( F '''' ( G '''' X ) ) ) )
20 17 19 anbi12d 
 |-  ( ( y = ( F '''' ( G '''' X ) ) /\ z = ( G '''' X ) ) -> ( ( X G z /\ z F y ) <-> ( X G ( G '''' X ) /\ ( G '''' X ) F ( F '''' ( G '''' X ) ) ) ) )
21 20 spc2egv 
 |-  ( ( ( F '''' ( G '''' X ) ) e. _V /\ ( G '''' X ) e. dom F ) -> ( ( X G ( G '''' X ) /\ ( G '''' X ) F ( F '''' ( G '''' X ) ) ) -> E. y E. z ( X G z /\ z F y ) ) )
22 11 15 21 syl2anc 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( X G ( G '''' X ) /\ ( G '''' X ) F ( F '''' ( G '''' X ) ) ) -> E. y E. z ( X G z /\ z F y ) ) )
23 7 14 22 mp2and 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E. y E. z ( X G z /\ z F y ) )
24 dfdfat2 
 |-  ( G defAt X <-> ( X e. dom G /\ E! z X G z ) )
25 tz6.12c-afv2 
 |-  ( E! z X G z -> ( ( G '''' X ) = z <-> X G z ) )
26 25 adantl 
 |-  ( ( X e. dom G /\ E! z X G z ) -> ( ( G '''' X ) = z <-> X G z ) )
27 24 26 sylbi 
 |-  ( G defAt X -> ( ( G '''' X ) = z <-> X G z ) )
28 27 adantr 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( G '''' X ) = z <-> X G z ) )
29 breq1 
 |-  ( ( G '''' X ) = z -> ( ( G '''' X ) F y <-> z F y ) )
30 29 adantl 
 |-  ( ( F defAt ( G '''' X ) /\ ( G '''' X ) = z ) -> ( ( G '''' X ) F y <-> z F y ) )
31 30 exbiri 
 |-  ( F defAt ( G '''' X ) -> ( ( G '''' X ) = z -> ( z F y -> ( G '''' X ) F y ) ) )
32 31 adantl 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( G '''' X ) = z -> ( z F y -> ( G '''' X ) F y ) ) )
33 28 32 sylbird 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( X G z -> ( z F y -> ( G '''' X ) F y ) ) )
34 33 impd 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( X G z /\ z F y ) -> ( G '''' X ) F y ) )
35 34 exlimdv 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( E. z ( X G z /\ z F y ) -> ( G '''' X ) F y ) )
36 35 alrimiv 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> A. y ( E. z ( X G z /\ z F y ) -> ( G '''' X ) F y ) )
37 euim 
 |-  ( ( E. y E. z ( X G z /\ z F y ) /\ A. y ( E. z ( X G z /\ z F y ) -> ( G '''' X ) F y ) ) -> ( E! y ( G '''' X ) F y -> E! y E. z ( X G z /\ z F y ) ) )
38 23 36 37 syl2anc 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( E! y ( G '''' X ) F y -> E! y E. z ( X G z /\ z F y ) ) )
39 38 com12 
 |-  ( E! y ( G '''' X ) F y -> ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E! y E. z ( X G z /\ z F y ) ) )
40 39 adantl 
 |-  ( ( ( G '''' X ) e. dom F /\ E! y ( G '''' X ) F y ) -> ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E! y E. z ( X G z /\ z F y ) ) )
41 40 adantl 
 |-  ( ( G defAt X /\ ( ( G '''' X ) e. dom F /\ E! y ( G '''' X ) F y ) ) -> ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E! y E. z ( X G z /\ z F y ) ) )
42 1 41 sylan2b 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E! y E. z ( X G z /\ z F y ) ) )
43 42 pm2.43i 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E! y E. z ( X G z /\ z F y ) )
44 df-dfat 
 |-  ( G defAt X <-> ( X e. dom G /\ Fun ( G |` { X } ) ) )
45 44 simplbi 
 |-  ( G defAt X -> X e. dom G )
46 vex 
 |-  y e. _V
47 46 a1i 
 |-  ( F defAt ( G '''' X ) -> y e. _V )
48 brcog 
 |-  ( ( X e. dom G /\ y e. _V ) -> ( X ( F o. G ) y <-> E. z ( X G z /\ z F y ) ) )
49 45 47 48 syl2an 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( X ( F o. G ) y <-> E. z ( X G z /\ z F y ) ) )
50 49 eubidv 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( E! y X ( F o. G ) y <-> E! y E. z ( X G z /\ z F y ) ) )
51 43 50 mpbird 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E! y X ( F o. G ) y )