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	Could not format assertion : No typesetting found for |- ( ( A e. On /\ ( _K3 ` A ) = (/) ) -> ( _FL ` A ) = ( _FL " A ) ) with typecode |-

Proof

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