Theorem fprlem1 8281

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 3454	. . . . 5 ⊢ 𝑥 ∈ V
2		vex 3454	. . . . 5 ⊢ 𝑢 ∈ V
3	1, 2	breldm 5874	. . . 4 ⊢ (𝑥𝑔𝑢 → 𝑥 ∈ dom 𝑔)
4		vex 3454	. . . . 5 ⊢ 𝑣 ∈ V
5	1, 4	breldm 5874	. . . 4 ⊢ (𝑥ℎ𝑣 → 𝑥 ∈ dom ℎ)
6		elin 3932	. . . . 5 ⊢ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ↔ (𝑥 ∈ dom 𝑔 ∧ 𝑥 ∈ dom ℎ))
7	6	biimpri 228	. . . 4 ⊢ ((𝑥 ∈ dom 𝑔 ∧ 𝑥 ∈ dom ℎ) → 𝑥 ∈ (dom 𝑔 ∩ dom ℎ))
8	3, 5, 7	syl2an 596	. . 3 ⊢ ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑥 ∈ (dom 𝑔 ∩ dom ℎ))
9		id 22	. . 3 ⊢ ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣))
10	2	brresi 5961	. . . . 5 ⊢ (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥𝑔𝑢))
11	4	brresi 5961	. . . . 5 ⊢ (𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣 ↔ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥ℎ𝑣))
12	10, 11	anbi12i 628	. . . 4 ⊢ ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥ℎ𝑣)))
13		an4 656	. . . 4 ⊢ (((𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥𝑔𝑢) ∧ (𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥ℎ𝑣)) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥 ∈ (dom 𝑔 ∩ dom ℎ)) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)))
14	12, 13	bitri 275	. . 3 ⊢ ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣) ↔ ((𝑥 ∈ (dom 𝑔 ∩ dom ℎ) ∧ 𝑥 ∈ (dom 𝑔 ∩ dom ℎ)) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)))
15	8, 8, 9, 14	syl21anbrc 1345	. 2 ⊢ ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣))
16		inss2 4203	. . . . . . . . . 10 ⊢ (dom 𝑔 ∩ dom ℎ) ⊆ dom ℎ
17		fprlem.1	. . . . . . . . . . 11 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
18	17	frrlem3 8269	. . . . . . . . . 10 ⊢ (ℎ ∈ 𝐵 → dom ℎ ⊆ 𝐴)
19	16, 18	sstrid 3960	. . . . . . . . 9 ⊢ (ℎ ∈ 𝐵 → (dom 𝑔 ∩ dom ℎ) ⊆ 𝐴)
20	19	adantl 481	. . . . . . . 8 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (dom 𝑔 ∩ dom ℎ) ⊆ 𝐴)
21	20	adantl 481	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → (dom 𝑔 ∩ dom ℎ) ⊆ 𝐴)
22		simpl1 1192	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Fr 𝐴)
23		frss 5604	. . . . . . 7 ⊢ ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 → (𝑅 Fr 𝐴 → 𝑅 Fr (dom 𝑔 ∩ dom ℎ)))
24	21, 22, 23	sylc 65	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Fr (dom 𝑔 ∩ dom ℎ))
25		simpl2 1193	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Po 𝐴)
26		poss 5550	. . . . . . 7 ⊢ ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 → (𝑅 Po 𝐴 → 𝑅 Po (dom 𝑔 ∩ dom ℎ)))
27	21, 25, 26	sylc 65	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Po (dom 𝑔 ∩ dom ℎ))
28		simpl3 1194	. . . . . . 7 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Se 𝐴)
29		sess2 5606	. . . . . . 7 ⊢ ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 → (𝑅 Se 𝐴 → 𝑅 Se (dom 𝑔 ∩ dom ℎ)))
30	21, 28, 29	sylc 65	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → 𝑅 Se (dom 𝑔 ∩ dom ℎ))
31	17	frrlem4 8270	. . . . . . 7 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
32	31	adantl 481	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
33	17	frrlem4 8270	. . . . . . . . 9 ⊢ ((ℎ ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((ℎ ↾ (dom ℎ ∩ dom 𝑔)) Fn (dom ℎ ∩ dom 𝑔) ∧ ∀𝑎 ∈ (dom ℎ ∩ dom 𝑔)((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎)))))
34		incom 4174	. . . . . . . . . . . 12 ⊢ (dom 𝑔 ∩ dom ℎ) = (dom ℎ ∩ dom 𝑔)
35	34	reseq2i 5949	. . . . . . . . . . 11 ⊢ (ℎ ↾ (dom 𝑔 ∩ dom ℎ)) = (ℎ ↾ (dom ℎ ∩ dom 𝑔))
36		fneq12 6616	. . . . . . . . . . 11 ⊢ (((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) = (ℎ ↾ (dom ℎ ∩ dom 𝑔)) ∧ (dom 𝑔 ∩ dom ℎ) = (dom ℎ ∩ dom 𝑔)) → ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ↔ (ℎ ↾ (dom ℎ ∩ dom 𝑔)) Fn (dom ℎ ∩ dom 𝑔)))
37	35, 34, 36	mp2an 692	. . . . . . . . . 10 ⊢ ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ↔ (ℎ ↾ (dom ℎ ∩ dom 𝑔)) Fn (dom ℎ ∩ dom 𝑔))
38	35	fveq1i 6861	. . . . . . . . . . . 12 ⊢ ((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = ((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎)
39		predeq2 6279	. . . . . . . . . . . . . . 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 5950	. . . . . . . . . . . . 13 ⊢ ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = ((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎))
42	41	oveq2i 7400	. . . . . . . . . . . 12 ⊢ (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎)))
43	38, 42	eqeq12i 2748	. . . . . . . . . . 11 ⊢ (((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) ↔ ((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎))))
44	34, 43	raleqbii 3319	. . . . . . . . . 10 ⊢ (∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) ↔ ∀𝑎 ∈ (dom ℎ ∩ dom 𝑔)((ℎ ↾ (dom ℎ ∩ dom 𝑔))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom ℎ ∩ dom 𝑔)) ↾ Pred(𝑅, (dom ℎ ∩ dom 𝑔), 𝑎))))
45	37, 44	anbi12i 628	. . . . . . . . 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 234	. . . . . . . 8 ⊢ ((ℎ ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
47	46	ancoms 458	. . . . . . 7 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
48	47	adantl 481	. . . . . 6 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((ℎ ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((ℎ ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))
49		fpr3g 8266	. . . . . 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 1386	. . . . 5 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) = (ℎ ↾ (dom 𝑔 ∩ dom ℎ)))
51	50	breqd 5120	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → (𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣 ↔ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣))
52	51	biimprd 248	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → (𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣 → 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣))
53	17	frrlem2 8268	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔)
54	53	ad2antrl 728	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → Fun 𝑔)
55		funres 6560	. . . 4 ⊢ (Fun 𝑔 → Fun (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)))
56		dffun2 6523	. . . . 5 ⊢ (Fun (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↔ (Rel (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ∧ ∀𝑥∀𝑢∀𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣)))
57		2sp 2187	. . . . . 6 ⊢ (∀𝑢∀𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
58	57	sps 2186	. . . . 5 ⊢ (∀𝑥∀𝑢∀𝑣((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
59	56, 58	simplbiim 504	. . . 4 ⊢ (Fun (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
60	54, 55, 59	3syl 18	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
61	52, 60	sylan2d 605	. 2 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥(𝑔 ↾ (dom 𝑔 ∩ dom ℎ))𝑢 ∧ 𝑥(ℎ ↾ (dom 𝑔 ∩ dom ℎ))𝑣) → 𝑢 = 𝑣))
62	15, 61	syl5 34	1 ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2708  ∀wral 3045   ∩ cin 3915   ⊆ wss 3916   class class class wbr 5109   Po wpo 5546   Fr wfr 5590   Se wse 5591  dom cdm 5640   ↾ cres 5642  Rel wrel 5645  Predcpred 6275  Fun wfun 6507   Fn wfn 6508  ‘cfv 6513  (class class class)co 7389  frecscfrecs 8261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-fr 5593  df-se 5594  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6276  df-iota 6466  df-fun 6515  df-fn 6516  df-fv 6521  df-ov 7392

This theorem is referenced by:  fpr2a  8283  fpr1  8284  fprfung  8290