Theorem tfrlem5 8010

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 3497	. . 3 ⊢ 𝑔 ∈ V
3	1, 2	tfrlem3a 8007	. 2 ⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))))
4		vex 3497	. . 3 ⊢ ℎ ∈ V
5	1, 4	tfrlem3a 8007	. 2 ⊢ (ℎ ∈ 𝐴 ↔ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))
6		reeanv 3367	. . 3 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))))
7		fveq2 6664	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑔‘𝑎) = (𝑔‘𝑥))
8		fveq2 6664	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (ℎ‘𝑎) = (ℎ‘𝑥))
9	7, 8	eqeq12d 2837	. . . . . . 7 ⊢ (𝑎 = 𝑥 → ((𝑔‘𝑎) = (ℎ‘𝑎) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
10		onin 6216	. . . . . . . . 9 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∩ 𝑤) ∈ On)
11	10	3ad2ant1 1129	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ∈ On)
12		simp2ll 1236	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑔 Fn 𝑧)
13		fnfun 6447	. . . . . . . . . 10 ⊢ (𝑔 Fn 𝑧 → Fun 𝑔)
14	12, 13	syl 17	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun 𝑔)
15		inss1 4204	. . . . . . . . . 10 ⊢ (𝑧 ∩ 𝑤) ⊆ 𝑧
16		fndm 6449	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
17	12, 16	syl 17	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom 𝑔 = 𝑧)
18	15, 17	sseqtrrid 4019	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom 𝑔)
19	14, 18	jca 514	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun 𝑔 ∧ (𝑧 ∩ 𝑤) ⊆ dom 𝑔))
20		simp2rl 1238	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ℎ Fn 𝑤)
21		fnfun 6447	. . . . . . . . . 10 ⊢ (ℎ Fn 𝑤 → Fun ℎ)
22	20, 21	syl 17	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun ℎ)
23		inss2 4205	. . . . . . . . . 10 ⊢ (𝑧 ∩ 𝑤) ⊆ 𝑤
24		fndm 6449	. . . . . . . . . . 11 ⊢ (ℎ Fn 𝑤 → dom ℎ = 𝑤)
25	20, 24	syl 17	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom ℎ = 𝑤)
26	23, 25	sseqtrrid 4019	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom ℎ)
27	22, 26	jca 514	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun ℎ ∧ (𝑧 ∩ 𝑤) ⊆ dom ℎ))
28		simp2lr 1237	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))
29		ssralv 4032	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑧 → (∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))))
30	15, 28, 29	mpsyl 68	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))
31		simp2rr 1239	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))
32		ssralv 4032	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑤 → (∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))
33	23, 31, 32	mpsyl 68	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))
34	11, 19, 27, 30, 33	tfrlem1 8006	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (ℎ‘𝑎))
35		simp3l 1197	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥𝑔𝑢)
36		fnbr 6453	. . . . . . . . 9 ⊢ ((𝑔 Fn 𝑧 ∧ 𝑥𝑔𝑢) → 𝑥 ∈ 𝑧)
37	12, 35, 36	syl2anc 586	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑧)
38		simp3r 1198	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥ℎ𝑣)
39		fnbr 6453	. . . . . . . . 9 ⊢ ((ℎ Fn 𝑤 ∧ 𝑥ℎ𝑣) → 𝑥 ∈ 𝑤)
40	20, 38, 39	syl2anc 586	. . . . . . . 8 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑤)
41	37, 40	elind 4170	. . . . . . 7 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ (𝑧 ∩ 𝑤))
42	9, 34, 41	rspcdva 3624	. . . . . 6 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = (ℎ‘𝑥))
43		funbrfv 6710	. . . . . . 7 ⊢ (Fun 𝑔 → (𝑥𝑔𝑢 → (𝑔‘𝑥) = 𝑢))
44	14, 35, 43	sylc 65	. . . . . 6 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = 𝑢)
45		funbrfv 6710	. . . . . . 7 ⊢ (Fun ℎ → (𝑥ℎ𝑣 → (ℎ‘𝑥) = 𝑣))
46	22, 38, 45	sylc 65	. . . . . 6 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (ℎ‘𝑥) = 𝑣)
47	42, 44, 46	3eqtr3d 2864	. . . . 5 ⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑢 = 𝑣)
48	47	3exp 1115	. . . 4 ⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)))
49	48	rexlimivv 3292	. . 3 ⊢ (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
50	6, 49	sylbir 237	. 2 ⊢ ((∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
51	3, 5, 50	syl2anb 599	1 ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  {cab 2799  ∀wral 3138  ∃wrex 3139   ∩ cin 3934   ⊆ wss 3935   class class class wbr 5058  dom cdm 5549   ↾ cres 5551  Oncon0 6185  Fun wfun 6343   Fn wfn 6344  ‘cfv 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-ord 6188  df-on 6189  df-iota 6308  df-fun 6351  df-fn 6352  df-fv 6357

This theorem is referenced by:  tfrlem7  8013