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 8105

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 8103	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔)
3	2	funfnd 6465	. . . 4 ⊢ (𝑔 ∈ 𝐵 → 𝑔 Fn dom 𝑔)
4		fnresin1 6557	. . . 4 ⊢ (𝑔 Fn dom 𝑔 → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
5	3, 4	syl 17	. . 3 ⊢ (𝑔 ∈ 𝐵 → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
6	5	adantr 481	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
7	1	frrlem1 8102	. . . . . . . 8 ⊢ 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))}
8	7	abeq2i 2875	. . . . . . 7 ⊢ (𝑔 ∈ 𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
9		fndm 6536	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
10	9	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)) → dom 𝑔 = 𝑏)
11	10	raleqdv 3348	. . . . . . . . . 10 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏)) → (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ↔ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
12	11	biimp3ar 1469	. . . . . . . . 9 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
13		rsp 3131	. . . . . . . . 9 ⊢ (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
14	12, 13	syl 17	. . . . . . . 8 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
15	14	exlimiv 1933	. . . . . . 7 ⊢ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
16	8, 15	sylbi 216	. . . . . 6 ⊢ (𝑔 ∈ 𝐵 → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
17		elinel1 4129	. . . . . 6 ⊢ (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → 𝑎 ∈ dom 𝑔)
18	16, 17	impel 506	. . . . 5 ⊢ ((𝑔 ∈ 𝐵 ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
19	18	adantlr 712	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
20		simpr 485	. . . . 5 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → 𝑎 ∈ (dom 𝑔 ∩ dom ℎ))
21	20	fvresd 6794	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑔‘𝑎))
22		resres 5904	. . . . . 6 ⊢ ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))
23		predss 6210	. . . . . . . . 9 ⊢ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)
24		sseqin2 4149	. . . . . . . . 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 8102	. . . . . . . . . . . 12 ⊢ 𝐵 = {ℎ ∣ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))}
27	26	abeq2i 2875	. . . . . . . . . . 11 ⊢ (ℎ ∈ 𝐵 ↔ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎)))))
28		exdistrv 1959	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
29		inss1 4162	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∩ 𝑐) ⊆ 𝑏
30		simpl2l 1225	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑏 ⊆ 𝐴)
31	29, 30	sstrid 3932	. . . . . . . . . . . . . 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 3144	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
35		nfra1 3144	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
36	34, 35	nfan 1902	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎(∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
37		elinel1 4129	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑏)
38		rsp 3131	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎 ∈ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
39	37, 38	syl5com 31	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
40		elinel2 4130	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑐)
41		rsp 3131	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎 ∈ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
42	40, 41	syl5com 31	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
43	39, 42	anim12d 609	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
44		ssin 4164	. . . . . . . . . . . . . . . . . 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 3141	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
48	32, 33, 47	syl2an 596	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
49		simpl1 1190	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → 𝑔 Fn 𝑏)
50	49	fndmd 6538	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → dom 𝑔 = 𝑏)
51		simpr1 1193	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ℎ Fn 𝑐)
52	51	fndmd 6538	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝑎𝐺(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → dom ℎ = 𝑐)
53		ineq12 4141	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → (dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐))
54	53	sseq1d 3952	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ↔ (𝑏 ∩ 𝑐) ⊆ 𝐴))
55	53	sseq2d 3953	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
56	53, 55	raleqbidv 3336	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
57	54, 56	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑔 = 𝑏 ∧ dom ℎ = 𝑐) → (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) ↔ ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))))
58	50, 52, 57	syl2anc 584	. . . . . . . . . . . . . 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 1935	. . . . . . . . . . . 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 598	. . . . . . . . . 10 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
63	62	adantr 481	. . . . . . . . 9 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
64		preddowncl 6235	. . . . . . . . 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 2790	. . . . . . 7 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
67	66	reseq2d 5891	. . . . . 6 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
68	22, 67	eqtrid 2790	. . . . 5 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
69	68	oveq2d 7291	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑎𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
70	19, 21, 69	3eqtr4d 2788	. . 3 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
71	70	ralrimiva 3103	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
72	6, 71	jca 512	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 396 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2106 {cab 2715 ∀wral 3064 ∩ cin 3886 ⊆ wss 3887 dom cdm 5589 ↾ cres 5591 Predcpred 6201 Fn wfn 6428 ‘cfv 6433 (class class class)co 7275

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-iota 6391 df-fun 6435 df-fn 6436 df-fv 6441 df-ov 7278

This theorem is referenced by: fprlem1 8116 frrlem15 9515

W3C validator