Theorem tfrlem5 6545

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 2816	. . 3 ⊢ 𝑔 ∈ V
3	1, 2	tfrlem3a 6541	. 2 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))))
4		vex 2816	. . 3 ⊢ ℎ ∈ V
5	1, 4	tfrlem3a 6541	. 2 ⊢ (ℎ ∈ 𝐴 ↔ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))
6		reeanv 2713	. . 3 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))))
7		fveq2 5670	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (𝑔‘𝑎) = (𝑔‘𝑥))
8		fveq2 5670	. . . . . . . . 9 ⊢ (𝑎 = 𝑥 → (ℎ‘𝑎) = (ℎ‘𝑥))
9	7, 8	eqeq12d 2247	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → ((𝑔‘𝑎) = (ℎ‘𝑎) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
10		onin 4507	. . . . . . . . . 10 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∩ 𝑤) ∈ On)
11	10	3ad2ant1 1045	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ∈ On)
12		simp2ll 1091	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑔 Fn 𝑧)
13		fnfun 5453	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑧 → Fun 𝑔)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun 𝑔)
15		inss1 3441	. . . . . . . . . . 11 ⊢ (𝑧 ∩ 𝑤) ⊆ 𝑧
16		fndm 5455	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
17	12, 16	syl 14	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom 𝑔 = 𝑧)
18	15, 17	sseqtrrid 3289	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom 𝑔)
19	14, 18	jca 306	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun 𝑔 ∧ (𝑧 ∩ 𝑤) ⊆ dom 𝑔))
20		simp2rl 1093	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ℎ Fn 𝑤)
21		fnfun 5453	. . . . . . . . . . 11 ⊢ (ℎ Fn 𝑤 → Fun ℎ)
22	20, 21	syl 14	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun ℎ)
23		inss2 3442	. . . . . . . . . . 11 ⊢ (𝑧 ∩ 𝑤) ⊆ 𝑤
24		fndm 5455	. . . . . . . . . . . 12 ⊢ (ℎ Fn 𝑤 → dom ℎ = 𝑤)
25	20, 24	syl 14	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom ℎ = 𝑤)
26	23, 25	sseqtrrid 3289	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom ℎ)
27	22, 26	jca 306	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun ℎ ∧ (𝑧 ∩ 𝑤) ⊆ dom ℎ))
28		simp2lr 1092	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))
29		ssralv 3302	. . . . . . . . . 10 ⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑧 → (∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))))
30	15, 28, 29	mpsyl 65	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))
31		simp2rr 1094	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))
32		ssralv 3302	. . . . . . . . . 10 ⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑤 → (∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))
33	23, 31, 32	mpsyl 65	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))
34	11, 19, 27, 30, 33	tfrlem1 6539	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (ℎ‘𝑎))
35		simp3l 1052	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥𝑔𝑢)
36		fnbr 5460	. . . . . . . . . 10 ⊢ ((𝑔 Fn 𝑧 ∧ 𝑥𝑔𝑢) → 𝑥 ∈ 𝑧)
37	12, 35, 36	syl2anc 411	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑧)
38		simp3r 1053	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥ℎ𝑣)
39		fnbr 5460	. . . . . . . . . 10 ⊢ ((ℎ Fn 𝑤 ∧ 𝑥ℎ𝑣) → 𝑥 ∈ 𝑤)
40	20, 38, 39	syl2anc 411	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑤)
41		elin 3402	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤))
42	37, 40, 41	sylanbrc 417	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ (𝑧 ∩ 𝑤))
43	9, 34, 42	rspcdva 2926	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = (ℎ‘𝑥))
44		funbrfv 5713	. . . . . . . 8 ⊢ (Fun 𝑔 → (𝑥𝑔𝑢 → (𝑔‘𝑥) = 𝑢))
45	14, 35, 44	sylc 62	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = 𝑢)
46		funbrfv 5713	. . . . . . . 8 ⊢ (Fun ℎ → (𝑥ℎ𝑣 → (ℎ‘𝑥) = 𝑣))
47	22, 38, 46	sylc 62	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (ℎ‘𝑥) = 𝑣)
48	43, 45, 47	3eqtr3d 2273	. . . . . 6 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑢 = 𝑣)
49	48	3exp 1229	. . . . 5 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)))
50	49	rexlimdva 2660	. . . 4 ⊢ (𝑧 ∈ On → (∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)))
51	50	rexlimiv 2654	. . 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 1005   = wceq 1398   ∈ wcel 2203  {cab 2218  ∀wral 2520  ∃wrex 2521   ∩ cin 3210   ⊆ wss 3211   class class class wbr 4109  Oncon0 4484  dom cdm 4749   ↾ cres 4751  Fun wfun 5346   Fn wfn 5347  ‘cfv 5352

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-setind 4659

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-tr 4209  df-id 4414  df-iord 4487  df-on 4489  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-res 4761  df-iota 5312  df-fun 5354  df-fn 5355  df-fv 5360

This theorem is referenced by:  tfrlem7  6548  tfrexlem  6565