Metamath Proof Explorer

Theorem fnlfvk30

Description: The value of _FL when the value of _K3 is zero. Part of Proposition 15.14 of TakeutiZaring p. 158. (Contributed by BTernaryTau, 17-Oct-2026)

Ref Expression
Assertion fnlfvk30 
|- ( ( A e. On /\ ( _K3 ` A ) = (/) ) -> ( _FL ` A ) = ( _FL " A ) )

Proof

Step Hyp Ref Expression
1 df-fnl 
 |-  _FL = recs ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) )
2 1 tfr2 
 |-  ( A e. On -> ( _FL ` A ) = ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ` ( _FL |` A ) ) )
3 2 adantr 
 |-  ( ( A e. On /\ ( _K3 ` A ) = (/) ) -> ( _FL ` A ) = ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ` ( _FL |` A ) ) )
4 eqid 
 |-  ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) = ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) )
5 dmeq 
 |-  ( x = ( _FL |` A ) -> dom x = dom ( _FL |` A ) )
6 5 adantl 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> dom x = dom ( _FL |` A ) )
7 onss 
 |-  ( A e. On -> A C_ On )
8 1 tfr1 
 |-  _FL Fn On
9 8 fndmi 
 |-  dom _FL = On
10 9 sseq2i 
 |-  ( A C_ dom _FL <-> A C_ On )
11 ssdmres 
 |-  ( A C_ dom _FL <-> dom ( _FL |` A ) = A )
12 10 11 bitr3i 
 |-  ( A C_ On <-> dom ( _FL |` A ) = A )
13 7 12 sylib 
 |-  ( A e. On -> dom ( _FL |` A ) = A )
14 13 ad2antrr 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> dom ( _FL |` A ) = A )
15 6 14 eqtrd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> dom x = A )
16 15 fveq2d 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> ( _K3 ` dom x ) = ( _K3 ` A ) )
17 simplr 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> ( _K3 ` A ) = (/) )
18 16 17 eqtrd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> ( _K3 ` dom x ) = (/) )
19 18 iftrued 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) = ran x )
20 rneq 
 |-  ( x = ( _FL |` A ) -> ran x = ran ( _FL |` A ) )
21 df-ima 
 |-  ( _FL " A ) = ran ( _FL |` A )
22 20 21 eqtr4di 
 |-  ( x = ( _FL |` A ) -> ran x = ( _FL " A ) )
23 22 adantl 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> ran x = ( _FL " A ) )
24 19 23 eqtrd 
 |-  ( ( ( A e. On /\ ( _K3 ` A ) = (/) ) /\ x = ( _FL |` A ) ) -> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) = ( _FL " A ) )
25 fnfun 
 |-  ( _FL Fn On -> Fun _FL )
26 8 25 ax-mp 
 |-  Fun _FL
27 resfunexg 
 |-  ( ( Fun _FL /\ A e. On ) -> ( _FL |` A ) e. _V )
28 26 27 mpan 
 |-  ( A e. On -> ( _FL |` A ) e. _V )
29 28 adantr 
 |-  ( ( A e. On /\ ( _K3 ` A ) = (/) ) -> ( _FL |` A ) e. _V )
30 funimaexg 
 |-  ( ( Fun _FL /\ A e. On ) -> ( _FL " A ) e. _V )
31 26 30 mpan 
 |-  ( A e. On -> ( _FL " A ) e. _V )
32 31 adantr 
 |-  ( ( A e. On /\ ( _K3 ` A ) = (/) ) -> ( _FL " A ) e. _V )
33 4 24 29 32 fvmptd2 
 |-  ( ( A e. On /\ ( _K3 ` A ) = (/) ) -> ( ( x e. _V |-> if ( ( _K3 ` dom x ) = (/) , ran x , ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) ) ` ( _FL |` A ) ) = ( _FL " A ) )
34 3 33 eqtrd 
 |-  ( ( A e. On /\ ( _K3 ` A ) = (/) ) -> ( _FL ` A ) = ( _FL " A ) )