Theorem fprlem1 8303

Description: Lemma for well-founded recursion with a partial order. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023.)

Hypotheses

Ref	Expression
fprlem.1	⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
fprlem.2	⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)

Assertion

Ref	Expression
fprlem1	⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))

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

Allowed substitution hints:   𝐵(𝑥, 𝑦, 𝑣, 𝑢, 𝑓, 𝑔, ℎ)   𝐹(𝑥, 𝑦, 𝑣, 𝑢, 𝑓, 𝑔, ℎ)

Proof of Theorem fprlem1

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3461	. . . . 5 ⊢ 𝑥 ∈ V
2		vex 3461	. . . . 5 ⊢ 𝑢 ∈ V
3	1, 2	breldm 5900	. . . 4 ⊢ (𝑥𝑔𝑢 → 𝑥 ∈ dom 𝑔)
4		vex 3461	. . . . 5 ⊢ 𝑣 ∈ V
5	1, 4	breldm 5900	. . . 4 ⊢ (𝑥ℎ𝑣 → 𝑥 ∈ dom ℎ)
6		elin 3922	. . . . 5 ⊢ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ↔ (𝑥 ∈ dom 𝑔 ∧ 𝑥 ∈ dom ℎ))
7	6	biimpri 231	. . . 4 ⊢ ((𝑥 ∈ dom 𝑔 ∧ 𝑥 ∈ dom ℎ) → 𝑥 ∈ (dom 𝑔 ∩ dom ℎ))
8	3, 5, 7	syl2an 608	. . 3 ⊢ ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑥 ∈ (dom 𝑔 ∩ dom ℎ))
9		id 23	. . 3 ⊢ ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣))
10	2	brresi 5989	. . . . 5 ⊢ (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥𝑔𝑢))
11	4	brresi 5989	. . . . 5 ⊢ (𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥ℎ𝑣))
12	10, 11	anbi12i 640	. . . 4 ⊢ ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥ℎ𝑣)))
13		an4 669	. . . 4 ⊢ (((𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥ℎ𝑣)) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥 ∈ (dom 𝑔 ∩ dom ℎ)) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)))
14	12, 13	bitri 278	. . 3 ⊢ ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥 ∈ (dom 𝑔 ∩ dom ℎ)) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)))
15	8, 8, 9, 14	syl21anbrc 1363	. 2 ⊢ ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣))
16		inss2 4190	. . . . . . . . . 10 ⊢ (dom 𝑔 ∩ dom ℎ) ⊆ dom ℎ
17		fprlem.1	. . . . . . . . . . 11 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
18	17	frrlem3 8291	. . . . . . . . . 10 ⊢ (ℎ ∈ 𝐵 → dom ℎ ⊆ 𝐴)
19	16, 18	sstrid 3949	. . . . . . . . 9 ⊢ (ℎ ∈ 𝐵 → (dom 𝑔 ∩ dom ℎ) ⊆ 𝐴)
20	19	adantl 487	. . . . . . . 8 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (dom 𝑔 ∩ dom ℎ) ⊆ 𝐴)
21	20	adantl 487	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → (dom 𝑔 ∩ dom ℎ) ⊆ 𝐴)
22		simpl1 1210	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Fr 𝐴)
23		frss 5627	. . . . . . 7 ⊢ ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 → (𝑅 Fr 𝐴 → 𝑅 Fr (dom 𝑔 ∩ dom ℎ)))
24	21, 22, 23	sylc 66	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Fr (dom 𝑔 ∩ dom ℎ))
25		simpl2 1211	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Po 𝐴)
26		poss 5573	. . . . . . 7 ⊢ ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 → (𝑅 Po 𝐴 → 𝑅 Po (dom 𝑔 ∩ dom ℎ)))
27	21, 25, 26	sylc 66	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Po (dom 𝑔 ∩ dom ℎ))
28		simpl3 1212	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Se 𝐴)
29		sess2 5629	. . . . . . 7 ⊢ ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 → (𝑅 Se 𝐴 → 𝑅 Se (dom 𝑔 ∩ dom ℎ)))
30	21, 28, 29	sylc 66	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Se (dom 𝑔 ∩ dom ℎ))
31	17	frrlem4 8292	. . . . . . 7 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
32	31	adantl 487	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
33	17	frrlem4 8292	. . . . . . . . 9 ⊢ ((ℎ ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((ℎ ↾ (dom ℎ ∩ dom 𝑔)) Fn (dom ℎ ∩ dom 𝑔) ∧ ∀𝑎 ∈ (dom ℎ ∩ dom 𝑔)((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎)))))
34		incom 4162	. . . . . . . . . . . 12 ⊢ (dom 𝑔 ∩ dom ℎ) = (dom ℎ ∩ dom 𝑔)
35	34	reseq2i 5977	. . . . . . . . . . 11 ⊢ (ℎ ↾ (dom 𝑔 ∩ dom ℎ)) = (ℎ ↾ (dom ℎ ∩ dom 𝑔))
36		fneq12 6635	. . . . . . . . . . 11 ⊢ (((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) = (ℎ ↾ (dom ℎ ∩ dom 𝑔)) ∧ (dom 𝑔 ∩ dom ℎ) = (dom ℎ ∩ dom 𝑔)) → ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ↔ (ℎ ↾ (dom ℎ ∩ dom 𝑔)) Fn (dom ℎ ∩ dom 𝑔)))
37	35, 34, 36	mp2an 705	. . . . . . . . . 10 ⊢ ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ↔ (ℎ ↾ (dom ℎ ∩ dom 𝑔)) Fn (dom ℎ ∩ dom 𝑔))
38	35	fveq1i 6886	. . . . . . . . . . . 12 ⊢ ((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = ((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎)
39		predeq2 6309	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑔 ∩ dom ℎ) = (dom ℎ ∩ dom 𝑔) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎))
40	34, 39	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎)
41	35, 40	reseq12i 5978	. . . . . . . . . . . . 13 ⊢ ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = ((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎))
42	41	oveq2i 7430	. . . . . . . . . . . 12 ⊢ (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎)))
43	38, 42	eqeq12i 2783	. . . . . . . . . . 11 ⊢ (((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) ↔ ((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎))))
44	34, 43	raleqbii 3338	. . . . . . . . . 10 ⊢ (∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) ↔ ∀𝑎 ∈ (dom ℎ ∩ dom 𝑔)((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎))))
45	37, 44	anbi12i 640	. . . . . . . . 9 ⊢ (((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))) ↔ ((ℎ ↾ (dom ℎ ∩ dom 𝑔)) Fn (dom ℎ ∩ dom 𝑔) ∧ ∀𝑎 ∈ (dom ℎ ∩ dom 𝑔)((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎)))))
46	33, 45	sylibr 237	. . . . . . . 8 ⊢ ((ℎ ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
47	46	ancoms 464	. . . . . . 7 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
48	47	adantl 487	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
49		fpr3g 8288	. . . . . 6 ⊢ (((𝑅 Fr (dom 𝑔 ∩ dom ℎ) ∧ 𝑅 Po (dom 𝑔 ∩ dom ℎ) ∧ 𝑅 Se (dom 𝑔 ∩ dom ℎ)) ∧ ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))) ∧ ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))) → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) = (ℎ ↾ (dom 𝑔 ∩ dom ℎ)))
50	24, 27, 30, 32, 48, 49	syl311anc 1411	. . . . 5 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) = (ℎ ↾ (dom 𝑔 ∩ dom ℎ)))
51	50	breqd 5122	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣 ↔ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣))
52	51	biimprd 251	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → (𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣 → 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣))
53	17	frrlem2 8290	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔)
54	53	ad2antrl 741	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → Fun 𝑔)
55		funres 6582	. . . 4 ⊢ (Fun 𝑔 → Fun (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)))
56		dffun2 6550	. . . . 5 ⊢ (Fun (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↔ (Rel (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ∧ ∀𝑥∀𝑢∀𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣)))
57		2sp 2225	. . . . . 6 ⊢ (∀𝑢∀𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
58	57	sps 2224	. . . . 5 ⊢ (∀𝑥∀𝑢∀𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
59	56, 58	simplbiim 514	. . . 4 ⊢ (Fun (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
60	54, 55, 59	3syl 19	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
61	52, 60	sylan2d 617	. 2 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
62	15, 61	syl5 35	1 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {cab 2743  ∀wral 3081   ∩ cin 3905   ⊆ wss 3906   class class class wbr 5111   Po wpo 5569   Fr wfr 5613   Se wse 5614  dom cdm 5663   ↾ cres 5665  Rel wrel 5668  Predcpred 6305  Fun wfun 6534   Fn wfn 6535  ‘cfv 6540  (class class class)co 7419  frecscfrecs 8283

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-fr 5616  df-se 5617  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548  df-ov 7422

This theorem is used by:  fpr2a  8305  fpr1  8306  fprfung  8312