Metamath Proof Explorer

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 ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( 𝐹𝐿 ‘ 𝐴 ) = ( ℱ ‘ ⟨ ( 𝐾3 ‘ 𝐴 ) , ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) , ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 df-fnl ⊢ 𝐹𝐿 = recs ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) )
2 1 tfr2 ⊢ ( 𝐴 ∈ On → ( 𝐹𝐿 ‘ 𝐴 ) = ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) ‘ ( 𝐹𝐿 ↾ 𝐴 ) ) )
3 2 adantr ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( 𝐹𝐿 ‘ 𝐴 ) = ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) ‘ ( 𝐹𝐿 ↾ 𝐴 ) ) )
4 eqid ⊢ ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) = ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) )
5 dmeq ⊢ ( 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) → dom 𝑥 = dom ( 𝐹𝐿 ↾ 𝐴 ) )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → dom 𝑥 = dom ( 𝐹𝐿 ↾ 𝐴 ) )
7 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
8 1 tfr1 ⊢ 𝐹𝐿 Fn On
9 8 fndmi ⊢ dom 𝐹𝐿 = On
10 9 sseq2i ⊢ ( 𝐴 ⊆ dom 𝐹𝐿 ↔ 𝐴 ⊆ On )
11 ssdmres ⊢ ( 𝐴 ⊆ dom 𝐹𝐿 ↔ dom ( 𝐹𝐿 ↾ 𝐴 ) = 𝐴 )
12 10 11 bitr3i ⊢ ( 𝐴 ⊆ On ↔ dom ( 𝐹𝐿 ↾ 𝐴 ) = 𝐴 )
13 7 12 sylib ⊢ ( 𝐴 ∈ On → dom ( 𝐹𝐿 ↾ 𝐴 ) = 𝐴 )
14 13 ad2antrr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → dom ( 𝐹𝐿 ↾ 𝐴 ) = 𝐴 )
15 6 14 eqtrd ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → dom 𝑥 = 𝐴 )
16 15 fveq2d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝐾3 ‘ dom 𝑥 ) = ( 𝐾3 ‘ 𝐴 ) )
17 simplr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝐾3 ‘ 𝐴 ) ≠ ∅ )
18 16 17 eqnetrd ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝐾3 ‘ dom 𝑥 ) ≠ ∅ )
19 18 neneqd ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ¬ ( 𝐾3 ‘ dom 𝑥 ) = ∅ )
20 19 iffalsed ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) = ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) )
21 simpr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) )
22 15 fveq2d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝐾1 ‘ dom 𝑥 ) = ( 𝐾1 ‘ 𝐴 ) )
23 21 22 fveq12d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) = ( ( 𝐹𝐿 ↾ 𝐴 ) ‘ ( 𝐾1 ‘ 𝐴 ) ) )
24 k39o ⊢ ( 𝐾3 ‘ 𝐴 ) ∈ 9o
25 9on ⊢ 9o ∈ On
26 25 oneli ⊢ ( ( 𝐾3 ‘ 𝐴 ) ∈ 9o → ( 𝐾3 ‘ 𝐴 ) ∈ On )
27 24 26 ax-mp ⊢ ( 𝐾3 ‘ 𝐴 ) ∈ On
28 on0eln0 ⊢ ( ( 𝐾3 ‘ 𝐴 ) ∈ On → ( ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ↔ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) )
29 27 28 ax-mp ⊢ ( ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ↔ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ )
30 k3n0k1lt ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 𝐾1 ‘ 𝐴 ) ∈ 𝐴 )
31 29 30 sylan2br ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( 𝐾1 ‘ 𝐴 ) ∈ 𝐴 )
32 31 fvresd ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( ( 𝐹𝐿 ↾ 𝐴 ) ‘ ( 𝐾1 ‘ 𝐴 ) ) = ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) )
33 32 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( ( 𝐹𝐿 ↾ 𝐴 ) ‘ ( 𝐾1 ‘ 𝐴 ) ) = ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) )
34 23 33 eqtrd ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) = ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) )
35 15 fveq2d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝐾2 ‘ dom 𝑥 ) = ( 𝐾2 ‘ 𝐴 ) )
36 21 35 fveq12d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) = ( ( 𝐹𝐿 ↾ 𝐴 ) ‘ ( 𝐾2 ‘ 𝐴 ) ) )
37 k3n0k2lt ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 𝐾2 ‘ 𝐴 ) ∈ 𝐴 )
38 29 37 sylan2br ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( 𝐾2 ‘ 𝐴 ) ∈ 𝐴 )
39 38 fvresd ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( ( 𝐹𝐿 ↾ 𝐴 ) ‘ ( 𝐾2 ‘ 𝐴 ) ) = ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) )
40 39 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( ( 𝐹𝐿 ↾ 𝐴 ) ‘ ( 𝐾2 ‘ 𝐴 ) ) = ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) )
41 36 40 eqtrd ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) = ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) )
42 16 34 41 oteq123d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ = ⟨ ( 𝐾3 ‘ 𝐴 ) , ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) , ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) ⟩ )
43 42 fveq2d ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) = ( ℱ ‘ ⟨ ( 𝐾3 ‘ 𝐴 ) , ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) , ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) ⟩ ) )
44 20 43 eqtrd ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) ∧ 𝑥 = ( 𝐹𝐿 ↾ 𝐴 ) ) → if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) = ( ℱ ‘ ⟨ ( 𝐾3 ‘ 𝐴 ) , ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) , ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) ⟩ ) )
45 fnfun ⊢ ( 𝐹𝐿 Fn On → Fun 𝐹𝐿 )
46 8 45 ax-mp ⊢ Fun 𝐹𝐿
47 resfunexg ⊢ ( ( Fun 𝐹𝐿 ∧ 𝐴 ∈ On ) → ( 𝐹𝐿 ↾ 𝐴 ) ∈ V )
48 46 47 mpan ⊢ ( 𝐴 ∈ On → ( 𝐹𝐿 ↾ 𝐴 ) ∈ V )
49 48 adantr ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( 𝐹𝐿 ↾ 𝐴 ) ∈ V )
50 fvexd ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( ℱ ‘ ⟨ ( 𝐾3 ‘ 𝐴 ) , ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) , ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) ⟩ ) ∈ V )
51 4 44 49 50 fvmptd2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( ( 𝑥 ∈ V ↦ if ( ( 𝐾3 ‘ dom 𝑥 ) = ∅ , ran 𝑥 , ( ℱ ‘ ⟨ ( 𝐾3 ‘ dom 𝑥 ) , ( 𝑥 ‘ ( 𝐾1 ‘ dom 𝑥 ) ) , ( 𝑥 ‘ ( 𝐾2 ‘ dom 𝑥 ) ) ⟩ ) ) ) ‘ ( 𝐹𝐿 ↾ 𝐴 ) ) = ( ℱ ‘ ⟨ ( 𝐾3 ‘ 𝐴 ) , ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) , ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) ⟩ ) )
52 3 51 eqtrd ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐾3 ‘ 𝐴 ) ≠ ∅ ) → ( 𝐹𝐿 ‘ 𝐴 ) = ( ℱ ‘ ⟨ ( 𝐾3 ‘ 𝐴 ) , ( 𝐹𝐿 ‘ ( 𝐾1 ‘ 𝐴 ) ) , ( 𝐹𝐿 ‘ ( 𝐾2 ‘ 𝐴 ) ) ⟩ ) )