This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )