Theorem tfrlem5 6399

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.)

Hypothesis

Ref	Expression
tfrlem.1	⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}

Assertion

Ref	Expression
tfrlem5	⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))

Distinct variable groups:   𝑓,𝑔,𝑥,𝑦,ℎ,𝑢,𝑣,𝐹   𝐴,𝑔,ℎ

Allowed substitution hints:   𝐴(𝑥,𝑦,𝑣,𝑢,𝑓)

Proof of Theorem tfrlem5

Dummy variables 𝑧 𝑎 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfrlem.1	. . 3 ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
2		vex 2774	. . 3 ⊢ 𝑔 ∈ V
3	1, 2	tfrlem3a 6395	. 2 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))))
4		vex 2774	. . 3 ⊢ ℎ ∈ V
5	1, 4	tfrlem3a 6395	. 2 ⊢ (ℎ ∈ 𝐴 ↔ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))
6		reeanv 2675	. . 3 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))))
7		fveq2 5575	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (𝑔‘𝑎) = (𝑔‘𝑥))
8		fveq2 5575	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (ℎ‘𝑎) = (ℎ‘𝑥))
9	7, 8	eqeq12d 2219	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → ((𝑔‘𝑎) = (ℎ‘𝑎) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
10		onin 4432	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∩ 𝑤) ∈ On)
11	10	3ad2ant1 1020	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ∈ On)
12		simp2ll 1066	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑔 Fn 𝑧)
13		fnfun 5370	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑧 → Fun 𝑔)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun 𝑔)
15		inss1 3392	. . . . . . . . . . 11 ⊢ (𝑧 ∩ 𝑤) ⊆ 𝑧
16		fndm 5372	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
17	12, 16	syl 14	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom 𝑔 = 𝑧)
18	15, 17	sseqtrrid 3243	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom 𝑔)
19	14, 18	jca 306	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun 𝑔 ∧ (𝑧 ∩ 𝑤) ⊆ dom 𝑔))
20		simp2rl 1068	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ℎ Fn 𝑤)
21		fnfun 5370	. . . . . . . . . . 11 ⊢ (ℎ Fn 𝑤 → Fun ℎ)
22	20, 21	syl 14	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun ℎ)
23		inss2 3393	. . . . . . . . . . 11 ⊢ (𝑧 ∩ 𝑤) ⊆ 𝑤
24		fndm 5372	. . . . . . . . . . . 12 ⊢ (ℎ Fn 𝑤 → dom ℎ = 𝑤)
25	20, 24	syl 14	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom ℎ = 𝑤)
26	23, 25	sseqtrrid 3243	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom ℎ)
27	22, 26	jca 306	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun ℎ ∧ (𝑧 ∩ 𝑤) ⊆ dom ℎ))
28		simp2lr 1067	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))
29		ssralv 3256	. . . . . . . . . 10 ⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑧 → (∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))))
30	15, 28, 29	mpsyl 65	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))
31		simp2rr 1069	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))
32		ssralv 3256	. . . . . . . . . 10 ⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑤 → (∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))
33	23, 31, 32	mpsyl 65	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))
34	11, 19, 27, 30, 33	tfrlem1 6393	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (ℎ‘𝑎))
35		simp3l 1027	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥𝑔𝑢)
36		fnbr 5377	. . . . . . . . . 10 ⊢ ((𝑔 Fn 𝑧 ∧ 𝑥𝑔𝑢) → 𝑥 ∈ 𝑧)
37	12, 35, 36	syl2anc 411	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑧)
38		simp3r 1028	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥ℎ𝑣)
39		fnbr 5377	. . . . . . . . . 10 ⊢ ((ℎ Fn 𝑤 ∧ 𝑥ℎ𝑣) → 𝑥 ∈ 𝑤)
40	20, 38, 39	syl2anc 411	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑤)
41		elin 3355	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤))
42	37, 40, 41	sylanbrc 417	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ (𝑧 ∩ 𝑤))
43	9, 34, 42	rspcdva 2881	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = (ℎ‘𝑥))
44		funbrfv 5616	. . . . . . . 8 ⊢ (Fun 𝑔 → (𝑥𝑔𝑢 → (𝑔‘𝑥) = 𝑢))
45	14, 35, 44	sylc 62	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = 𝑢)
46		funbrfv 5616	. . . . . . . 8 ⊢ (Fun ℎ → (𝑥ℎ𝑣 → (ℎ‘𝑥) = 𝑣))
47	22, 38, 46	sylc 62	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (ℎ‘𝑥) = 𝑣)
48	43, 45, 47	3eqtr3d 2245	. . . . . 6 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑢 = 𝑣)
49	48	3exp 1204	. . . . 5 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)))
50	49	rexlimdva 2622	. . . 4 ⊢ (𝑧 ∈ On → (∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)))
51	50	rexlimiv 2616	. . 3 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
52	6, 51	sylbir 135	. 2 ⊢ ((∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
53	3, 5, 52	syl2anb 291	1 ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980   = wceq 1372   ∈ wcel 2175  {cab 2190  ∀wral 2483  ∃wrex 2484   ∩ cin 3164   ⊆ wss 3165   class class class wbr 4043  Oncon0 4409  dom cdm 4674   ↾ cres 4676  Fun wfun 5264   Fn wfn 5265  ‘cfv 5270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-setind 4584

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-sbc 2998  df-csb 3093  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-mpt 4106  df-tr 4142  df-id 4339  df-iord 4412  df-on 4414  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-res 4686  df-iota 5231  df-fun 5272  df-fn 5273  df-fv 5278

This theorem is referenced by:  tfrlem7  6402  tfrexlem  6419