frrlem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > frrlem4		Structured version Visualization version GIF version

Theorem frrlem4 8280

Description: Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012.)

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

**Assertion**
Ref	Expression
frrlem4	⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))

Distinct variable groups: 𝐴,𝑎,𝑓,𝑔 𝐴,ℎ,𝑥,𝑦,𝑎 𝐵,𝑎 𝑓,ℎ,𝑥,𝑦 𝐺,𝑎,𝑓,𝑔 ℎ,𝐺,𝑥,𝑦 𝑥,𝑔,𝑦 𝑅,𝑎,𝑓,𝑔 𝑅,ℎ,𝑥,𝑦 Allowed substitution hints: 𝐵(𝑥,𝑦,𝑓,𝑔,ℎ)

Proof of Theorem frrlem4 Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frrlem4.1	. . . . . 6 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2	1	frrlem2 8278	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔)
3	2	funfnd 6579	. . . 4 ⊢ (𝑔 ∈ 𝐵 → 𝑔 Fn dom 𝑔)
4		fnresin1 6675	. . . 4 ⊢ (𝑔 Fn dom 𝑔 → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
5	3, 4	syl 17	. . 3 ⊢ (𝑔 ∈ 𝐵 → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
6	5	adantr 480	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
7	1	frrlem1 8277	. . . . . . . 8 ⊢ 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))}
8	7	eqabri 2876	. . . . . . 7 ⊢ (𝑔 ∈ 𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
9		fndm 6652	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
10	9	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)) → dom 𝑔 = 𝑏)
11	10	raleqdv 3324	. . . . . . . . . 10 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)) → (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ↔ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
12	11	biimp3ar 1469	. . . . . . . . 9 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
13		rsp 3243	. . . . . . . . 9 ⊢ (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
14	12, 13	syl 17	. . . . . . . 8 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
15	14	exlimiv 1932	. . . . . . 7 ⊢ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
16	8, 15	sylbi 216	. . . . . 6 ⊢ (𝑔 ∈ 𝐵 → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
17		elinel1 4195	. . . . . 6 ⊢ (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → 𝑎 ∈ dom 𝑔)
18	16, 17	impel 505	. . . . 5 ⊢ ((𝑔 ∈ 𝐵 ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
19	18	adantlr 712	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
20		simpr 484	. . . . 5 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → 𝑎 ∈ (dom 𝑔 ∩ dom ℎ))
21	20	fvresd 6911	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑔‘𝑎))
22		resres 5994	. . . . . 6 ⊢ ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))
23		predss 6308	. . . . . . . . 9 ⊢ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)
24		sseqin2 4215	. . . . . . . . 9 ⊢ (Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))
25	23, 24	mpbi 229	. . . . . . . 8 ⊢ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)
26	1	frrlem1 8277	. . . . . . . . . . . 12 ⊢ 𝐵 = {ℎ ∣ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))}
27	26	eqabri 2876	. . . . . . . . . . 11 ⊢ (ℎ ∈ 𝐵 ↔ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎)))))
28		exdistrv 1958	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
29		inss1 4228	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∩ 𝑐) ⊆ 𝑏
30		simpl2l 1225	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑏 ⊆ 𝐴)
31	29, 30	sstrid 3993	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → (𝑏 ∩ 𝑐) ⊆ 𝐴)
32		simp2r 1199	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)
33		simp2r 1199	. . . . . . . . . . . . . . 15 ⊢ ((ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
34		nfra1 3280	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
35		nfra1 3280	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
36	34, 35	nfan 1901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎(∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
37		elinel1 4195	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑏)
38		rsp 3243	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎 ∈ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
39	37, 38	syl5com 31	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
40		elinel2 4196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑐)
41		rsp 3243	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎 ∈ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
42	40, 41	syl5com 31	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
43	39, 42	anim12d 608	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
44		ssin 4230	. . . . . . . . . . . . . . . . . 18 ⊢ ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
45	44	biimpi 215	. . . . . . . . . . . . . . . . 17 ⊢ ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
46	43, 45	syl6com 37	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (𝑎 ∈ (𝑏 ∩ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
47	36, 46	ralrimi 3253	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
48	32, 33, 47	syl2an 595	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
49		simpl1 1190	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑔 Fn 𝑏)
50	49	fndmd 6654	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → dom 𝑔 = 𝑏)
51		simpr1 1193	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ℎ Fn 𝑐)
52	51	fndmd 6654	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → dom ℎ = 𝑐)
53		ineq12 4207	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → (dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐))
54	53	sseq1d 4013	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ↔ (𝑏 ∩ 𝑐) ⊆ 𝐴))
55	53	sseq2d 4014	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
56	53, 55	raleqbidv 3341	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
57	54, 56	anbi12d 630	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) ↔ ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))))
58	50, 52, 57	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) ↔ ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))))
59	31, 48, 58	mpbir2and 710	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
60	59	exlimivv 1934	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
61	28, 60	sylbir 234	. . . . . . . . . . 11 ⊢ ((∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
62	8, 27, 61	syl2anb 597	. . . . . . . . . 10 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
63	62	adantr 480	. . . . . . . . 9 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
64		preddowncl 6333	. . . . . . . . 9 ⊢ (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) → (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, 𝐴, 𝑎)))
65	63, 20, 64	sylc 65	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, 𝐴, 𝑎))
66	25, 65	eqtrid 2783	. . . . . . 7 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
67	66	reseq2d 5981	. . . . . 6 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
68	22, 67	eqtrid 2783	. . . . 5 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
69	68	oveq2d 7428	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
70	19, 21, 69	3eqtr4d 2781	. . 3 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
71	70	ralrimiva 3145	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
72	6, 71	jca 511	1 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1780 ∈ wcel 2105 {cab 2708 ∀wral 3060 ∩ cin 3947 ⊆ wss 3948 dom cdm 5676 ↾ cres 5678 Predcpred 6299 Fn wfn 6538 ‘cfv 6543 (class class class)co 7412

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-iota 6495 df-fun 6545 df-fn 6546 df-fv 6551 df-ov 7415

This theorem is referenced by: fprlem1 8291 frrlem15 9758

W3C validator