Theorem fnlfvk3n0

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

	Ref	Expression
Assertion	fnlfvk3n0	Could not format assertion : No typesetting found for |- ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _FL ` A ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` 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	eqnetrd	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	neneqd	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 |-
20	19	iffalsed	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 ) ) >. ) ) = ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom 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 ) ) >. ) ) = ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) ) with typecode |-
21		simpr	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> x = ( _FL |` A ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> x = ( _FL |` A ) ) with typecode |-
22	15	fveq2d	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K1 ` dom x ) = ( _K1 ` A ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K1 ` dom x ) = ( _K1 ` A ) ) with typecode |-
23	21 22	fveq12d	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K1 ` dom x ) ) = ( ( _FL |` A ) ` ( _K1 ` A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K1 ` dom x ) ) = ( ( _FL |` A ) ` ( _K1 ` A ) ) ) with typecode |-
24		k39o	Could not format ( _K3 ` A ) e. 9o : No typesetting found for |- ( _K3 ` A ) e. 9o with typecode |-
25		9on	Could not format 9o e. On : No typesetting found for |- 9o e. On with typecode |-
26	25	oneli	Could not format ( ( _K3 ` A ) e. 9o -> ( _K3 ` A ) e. On ) : No typesetting found for |- ( ( _K3 ` A ) e. 9o -> ( _K3 ` A ) e. On ) with typecode |-
27	24 26	ax-mp	Could not format ( _K3 ` A ) e. On : No typesetting found for |- ( _K3 ` A ) e. On with typecode |-
28		on0eln0	Could not format ( ( _K3 ` A ) e. On -> ( (/) e. ( _K3 ` A ) <-> ( _K3 ` A ) =/= (/) ) ) : No typesetting found for |- ( ( _K3 ` A ) e. On -> ( (/) e. ( _K3 ` A ) <-> ( _K3 ` A ) =/= (/) ) ) with typecode |-
29	27 28	ax-mp	Could not format ( (/) e. ( _K3 ` A ) <-> ( _K3 ` A ) =/= (/) ) : No typesetting found for |- ( (/) e. ( _K3 ` A ) <-> ( _K3 ` A ) =/= (/) ) with typecode |-
30		k3n0k1lt	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K1 ` A ) e. A ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K1 ` A ) e. A ) with typecode |-
31	29 30	sylan2br	Could not format ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _K1 ` A ) e. A ) : No typesetting found for |- ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _K1 ` A ) e. A ) with typecode |-
32	31	fvresd	Could not format ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ( _FL |` A ) ` ( _K1 ` A ) ) = ( _FL ` ( _K1 ` A ) ) ) : No typesetting found for |- ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ( _FL |` A ) ` ( _K1 ` A ) ) = ( _FL ` ( _K1 ` A ) ) ) with typecode |-
33	32	adantr	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ( _FL |` A ) ` ( _K1 ` A ) ) = ( _FL ` ( _K1 ` A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ( _FL |` A ) ` ( _K1 ` A ) ) = ( _FL ` ( _K1 ` A ) ) ) with typecode |-
34	23 33	eqtrd	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K1 ` dom x ) ) = ( _FL ` ( _K1 ` A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K1 ` dom x ) ) = ( _FL ` ( _K1 ` A ) ) ) with typecode |-
35	15	fveq2d	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K2 ` dom x ) = ( _K2 ` A ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( _K2 ` dom x ) = ( _K2 ` A ) ) with typecode |-
36	21 35	fveq12d	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K2 ` dom x ) ) = ( ( _FL |` A ) ` ( _K2 ` A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K2 ` dom x ) ) = ( ( _FL |` A ) ` ( _K2 ` A ) ) ) with typecode |-
37		k3n0k2lt	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K2 ` A ) e. A ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K2 ` A ) e. A ) with typecode |-
38	29 37	sylan2br	Could not format ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _K2 ` A ) e. A ) : No typesetting found for |- ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _K2 ` A ) e. A ) with typecode |-
39	38	fvresd	Could not format ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ( _FL |` A ) ` ( _K2 ` A ) ) = ( _FL ` ( _K2 ` A ) ) ) : No typesetting found for |- ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ( _FL |` A ) ` ( _K2 ` A ) ) = ( _FL ` ( _K2 ` A ) ) ) with typecode |-
40	39	adantr	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ( _FL |` A ) ` ( _K2 ` A ) ) = ( _FL ` ( _K2 ` A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ( _FL |` A ) ` ( _K2 ` A ) ) = ( _FL ` ( _K2 ` A ) ) ) with typecode |-
41	36 40	eqtrd	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K2 ` dom x ) ) = ( _FL ` ( _K2 ` A ) ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( x ` ( _K2 ` dom x ) ) = ( _FL ` ( _K2 ` A ) ) ) with typecode |-
42	16 34 41	oteq123d	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. = <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. = <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) with typecode |-
43	42	fveq2d	Could not format ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) ) : No typesetting found for |- ( ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) /\ x = ( _FL |` A ) ) -> ( ~F ` <. ( _K3 ` dom x ) , ( x ` ( _K1 ` dom x ) ) , ( x ` ( _K2 ` dom x ) ) >. ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) ) with typecode |-
44	20 43	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 ) ) >. ) ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` 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 ) ) >. ) ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) ) with typecode |-
45		fnfun	Could not format ( _FL Fn On -> Fun _FL ) : No typesetting found for |- ( _FL Fn On -> Fun _FL ) with typecode |-
46	8 45	ax-mp	Could not format Fun _FL : No typesetting found for |- Fun _FL with typecode |-
47		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 |-
48	46 47	mpan	Could not format ( A e. On -> ( _FL |` A ) e. _V ) : No typesetting found for |- ( A e. On -> ( _FL |` A ) e. _V ) with typecode |-
49	48	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 |-
50		fvexd	Could not format ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) e. _V ) : No typesetting found for |- ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) e. _V ) with typecode |-
51	4 44 49 50	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 ) ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` 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 ) ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) ) with typecode |-
52	3 51	eqtrd	Could not format ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _FL ` A ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) ) : No typesetting found for |- ( ( A e. On /\ ( _K3 ` A ) =/= (/) ) -> ( _FL ` A ) = ( ~F ` <. ( _K3 ` A ) , ( _FL ` ( _K1 ` A ) ) , ( _FL ` ( _K2 ` A ) ) >. ) ) with typecode |-