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