Metamath Proof Explorer


Theorem tfrlem5

Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 24-May-2019)

Ref Expression
Hypothesis tfrlem.1 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓𝑦 ) ) ) }
Assertion tfrlem5 ( ( 𝑔𝐴𝐴 ) → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) )

Proof

Step Hyp Ref Expression
1 tfrlem.1 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝐹 ‘ ( 𝑓𝑦 ) ) ) }
2 vex 𝑔 ∈ V
3 1 2 tfrlem3a ( 𝑔𝐴 ↔ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) )
4 vex ∈ V
5 1 4 tfrlem3a ( 𝐴 ↔ ∃ 𝑤 ∈ On ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) )
6 reeanv ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ↔ ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ∃ 𝑤 ∈ On ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) )
7 fveq2 ( 𝑎 = 𝑥 → ( 𝑔𝑎 ) = ( 𝑔𝑥 ) )
8 fveq2 ( 𝑎 = 𝑥 → ( 𝑎 ) = ( 𝑥 ) )
9 7 8 eqeq12d ( 𝑎 = 𝑥 → ( ( 𝑔𝑎 ) = ( 𝑎 ) ↔ ( 𝑔𝑥 ) = ( 𝑥 ) ) )
10 onin ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧𝑤 ) ∈ On )
11 10 3ad2ant1 ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ( 𝑧𝑤 ) ∈ On )
12 simp2ll ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → 𝑔 Fn 𝑧 )
13 fnfun ( 𝑔 Fn 𝑧 → Fun 𝑔 )
14 12 13 syl ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → Fun 𝑔 )
15 inss1 ( 𝑧𝑤 ) ⊆ 𝑧
16 12 fndmd ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → dom 𝑔 = 𝑧 )
17 15 16 sseqtrrid ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ( 𝑧𝑤 ) ⊆ dom 𝑔 )
18 14 17 jca ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ( Fun 𝑔 ∧ ( 𝑧𝑤 ) ⊆ dom 𝑔 ) )
19 simp2rl ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → Fn 𝑤 )
20 fnfun ( Fn 𝑤 → Fun )
21 19 20 syl ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → Fun )
22 inss2 ( 𝑧𝑤 ) ⊆ 𝑤
23 19 fndmd ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → dom = 𝑤 )
24 22 23 sseqtrrid ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ( 𝑧𝑤 ) ⊆ dom )
25 21 24 jca ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ( Fun ∧ ( 𝑧𝑤 ) ⊆ dom ) )
26 simp2lr ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) )
27 ssralv ( ( 𝑧𝑤 ) ⊆ 𝑧 → ( ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) → ∀ 𝑎 ∈ ( 𝑧𝑤 ) ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) )
28 15 26 27 mpsyl ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧𝑤 ) ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) )
29 simp2rr ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) )
30 ssralv ( ( 𝑧𝑤 ) ⊆ 𝑤 → ( ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) → ∀ 𝑎 ∈ ( 𝑧𝑤 ) ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) )
31 22 29 30 mpsyl ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧𝑤 ) ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) )
32 11 18 25 28 31 tfrlem1 ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧𝑤 ) ( 𝑔𝑎 ) = ( 𝑎 ) )
33 simp3l ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → 𝑥 𝑔 𝑢 )
34 fnbr ( ( 𝑔 Fn 𝑧𝑥 𝑔 𝑢 ) → 𝑥𝑧 )
35 12 33 34 syl2anc ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → 𝑥𝑧 )
36 simp3r ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → 𝑥 𝑣 )
37 fnbr ( ( Fn 𝑤𝑥 𝑣 ) → 𝑥𝑤 )
38 19 36 37 syl2anc ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → 𝑥𝑤 )
39 35 38 elind ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → 𝑥 ∈ ( 𝑧𝑤 ) )
40 9 32 39 rspcdva ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ( 𝑔𝑥 ) = ( 𝑥 ) )
41 funbrfv ( Fun 𝑔 → ( 𝑥 𝑔 𝑢 → ( 𝑔𝑥 ) = 𝑢 ) )
42 14 33 41 sylc ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ( 𝑔𝑥 ) = 𝑢 )
43 funbrfv ( Fun → ( 𝑥 𝑣 → ( 𝑥 ) = 𝑣 ) )
44 21 36 43 sylc ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → ( 𝑥 ) = 𝑣 )
45 40 42 44 3eqtr3d ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢𝑥 𝑣 ) ) → 𝑢 = 𝑣 )
46 45 3exp ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) ) )
47 46 rexlimivv ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) )
48 6 47 sylbir ( ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎𝑧 ( 𝑔𝑎 ) = ( 𝐹 ‘ ( 𝑔𝑎 ) ) ) ∧ ∃ 𝑤 ∈ On ( Fn 𝑤 ∧ ∀ 𝑎𝑤 ( 𝑎 ) = ( 𝐹 ‘ ( 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) )
49 3 5 48 syl2anb ( ( 𝑔𝐴𝐴 ) → ( ( 𝑥 𝑔 𝑢𝑥 𝑣 ) → 𝑢 = 𝑣 ) )