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		fndm	⊢ ( 𝑔 Fn 𝑧 → dom 𝑔 = 𝑧 )
17	12 16	syl	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → dom 𝑔 = 𝑧 )
18	15 17	sseqtrrid	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑧 ∩ 𝑤 ) ⊆ dom 𝑔 )
19	14 18	jca	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( Fun 𝑔 ∧ ( 𝑧 ∩ 𝑤 ) ⊆ dom 𝑔 ) )
20		simp2rl	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ℎ Fn 𝑤 )
21		fnfun	⊢ ( ℎ Fn 𝑤 → Fun ℎ )
22	20 21	syl	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → Fun ℎ )
23		inss2	⊢ ( 𝑧 ∩ 𝑤 ) ⊆ 𝑤
24		fndm	⊢ ( ℎ Fn 𝑤 → dom ℎ = 𝑤 )
25	20 24	syl	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → dom ℎ = 𝑤 )
26	23 25	sseqtrrid	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑧 ∩ 𝑤 ) ⊆ dom ℎ )
27	22 26	jca	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( Fun ℎ ∧ ( 𝑧 ∩ 𝑤 ) ⊆ dom ℎ ) )
28		simp2lr	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) )
29		ssralv	⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ 𝑧 → ( ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) )
30	15 28 29	mpsyl	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) )
31		simp2rr	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) )
32		ssralv	⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ 𝑤 → ( ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) )
33	23 31 32	mpsyl	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) )
34	11 19 27 30 33	tfrlem1	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( 𝑔 ‘ 𝑎 ) = ( ℎ ‘ 𝑎 ) )
35		simp3l	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 𝑔 𝑢 )
36		fnbr	⊢ ( ( 𝑔 Fn 𝑧 ∧ 𝑥 𝑔 𝑢 ) → 𝑥 ∈ 𝑧 )
37	12 35 36	syl2anc	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 ∈ 𝑧 )
38		simp3r	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 ℎ 𝑣 )
39		fnbr	⊢ ( ( ℎ Fn 𝑤 ∧ 𝑥 ℎ 𝑣 ) → 𝑥 ∈ 𝑤 )
40	20 38 39	syl2anc	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 ∈ 𝑤 )
41	37 40	elind	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) )
42	9 34 41	rspcdva	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
43		funbrfv	⊢ ( Fun 𝑔 → ( 𝑥 𝑔 𝑢 → ( 𝑔 ‘ 𝑥 ) = 𝑢 ) )
44	14 35 43	sylc	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑔 ‘ 𝑥 ) = 𝑢 )
45		funbrfv	⊢ ( Fun ℎ → ( 𝑥 ℎ 𝑣 → ( ℎ ‘ 𝑥 ) = 𝑣 ) )
46	22 38 45	sylc	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( ℎ ‘ 𝑥 ) = 𝑣 )
47	42 44 46	3eqtr3d	⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑢 = 𝑣 )
48	47	3exp	⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) ) )
49	48	rexlimivv	⊢ ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
50	6 49	sylbir	⊢ ( ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ∃ 𝑤 ∈ On ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
51	3 5 50	syl2anb	⊢ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )