wfrlem4 - Metamath Proof Explorer

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

Theorem wfrlem4 7418

Description: Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another one. (Contributed by Scott Fenton, 21-Apr-2011.)

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

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

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

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

Step	Hyp	Ref	Expression
1		wfrlem4.2	. . . . . 6 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2	1	wfrlem2 7415	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔)
3		funfn 5918	. . . . 5 ⊢ (Fun 𝑔 ↔ 𝑔 Fn dom 𝑔)
4	2, 3	sylib 208	. . . 4 ⊢ (𝑔 ∈ 𝐵 → 𝑔 Fn dom 𝑔)
5		fnresin1 6005	. . . 4 ⊢ (𝑔 Fn dom 𝑔 → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
6	4, 5	syl 17	. . 3 ⊢ (𝑔 ∈ 𝐵 → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
7	6	adantr 481	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
8		inss1 3833	. . . . . . . 8 ⊢ (dom 𝑔 ∩ dom ℎ) ⊆ dom 𝑔
9	8	sseli 3599	. . . . . . 7 ⊢ (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → 𝑎 ∈ dom 𝑔)
10	1	wfrlem1 7414	. . . . . . . . 9 ⊢ 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))}
11	10	abeq2i 2735	. . . . . . . 8 ⊢ (𝑔 ∈ 𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
12		fndm 5990	. . . . . . . . . . . . 13 ⊢ (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
13	12	raleqdv 3144	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑏 → (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ↔ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
14	13	biimpar 502	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑏 ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
15		rsp 2929	. . . . . . . . . . 11 ⊢ (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝑔 Fn 𝑏 ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
17	16	3adant2 1080	. . . . . . . . 9 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
18	17	exlimiv 1858	. . . . . . . 8 ⊢ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
19	11, 18	sylbi 207	. . . . . . 7 ⊢ (𝑔 ∈ 𝐵 → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
20	9, 19	syl5 34	. . . . . 6 ⊢ (𝑔 ∈ 𝐵 → (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
21	20	imp 445	. . . . 5 ⊢ ((𝑔 ∈ 𝐵 ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
22	21	adantlr 751	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
23		fvres 6207	. . . . 5 ⊢ (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑔‘𝑎))
24	23	adantl 482	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑔‘𝑎))
25		resres 5409	. . . . . 6 ⊢ ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))
26		predss 5687	. . . . . . . . 9 ⊢ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)
27		sseqin2 3817	. . . . . . . . 9 ⊢ (Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))
28	26, 27	mpbi 220	. . . . . . . 8 ⊢ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)
29	1	wfrlem1 7414	. . . . . . . . . . . 12 ⊢ 𝐵 = {ℎ ∣ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))}
30	29	abeq2i 2735	. . . . . . . . . . 11 ⊢ (ℎ ∈ 𝐵 ↔ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎)))))
31		3an6 1409	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
32	31	2exbii 1775	. . . . . . . . . . . . 13 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ ∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
33		eeanv 2182	. . . . . . . . . . . . 13 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
34	32, 33	bitri 264	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
35		ssinss1 3841	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ⊆ 𝐴 → (𝑏 ∩ 𝑐) ⊆ 𝐴)
36	35	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → (𝑏 ∩ 𝑐) ⊆ 𝐴)
37		nfra1 2941	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
38		nfra1 2941	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
39	37, 38	nfan 1828	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎(∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
40		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∩ 𝑐) ⊆ 𝑏
41	40	sseli 3599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑏)
42		rsp 2929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎 ∈ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
43	41, 42	syl5com 31	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
44		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∩ 𝑐) ⊆ 𝑐
45	44	sseli 3599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑐)
46		rsp 2929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎 ∈ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
47	45, 46	syl5com 31	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
48	43, 47	anim12d 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
49		ssin 3835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
50	49	biimpi 206	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
51	48, 50	syl6com 37	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (𝑎 ∈ (𝑏 ∩ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
52	39, 51	ralrimi 2957	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
53	52	ad2ant2l 782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
54	36, 53	jca 554	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
55		fndm 5990	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ Fn 𝑐 → dom ℎ = 𝑐)
56	12, 55	ineqan12d 3816	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) → (dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐))
57		sseq1 3626	. . . . . . . . . . . . . . . . . . 19 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ↔ (𝑏 ∩ 𝑐) ⊆ 𝐴))
58		sseq2 3627	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
59	58	raleqbi1dv 3146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
60	57, 59	anbi12d 747	. . . . . . . . . . . . . . . . . 18 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) ↔ ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))))
61	60	imbi2d 330	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → ((((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ))) ↔ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))))
62	56, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) → ((((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ))) ↔ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))))
63	54, 62	mpbiri 248	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) → (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ))))
64	63	imp 445	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
65	64	3adant3 1081	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
66	65	exlimivv 1860	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
67	34, 66	sylbir 225	. . . . . . . . . . 11 ⊢ ((∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
68	11, 30, 67	syl2anb 496	. . . . . . . . . 10 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
69	68	adantr 481	. . . . . . . . 9 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
70		simpr 477	. . . . . . . . 9 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → 𝑎 ∈ (dom 𝑔 ∩ dom ℎ))
71		preddowncl 5707	. . . . . . . . 9 ⊢ (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) → (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, 𝐴, 𝑎)))
72	69, 70, 71	sylc 65	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, 𝐴, 𝑎))
73	28, 72	syl5eq 2668	. . . . . . 7 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
74	73	reseq2d 5396	. . . . . 6 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
75	25, 74	syl5eq 2668	. . . . 5 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
76	75	fveq2d 6195	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
77	22, 24, 76	3eqtr4d 2666	. . 3 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
78	77	ralrimiva 2966	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
79	7, 78	jca 554	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 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 {cab 2608 ∀wral 2912 ∩ cin 3573 ⊆ wss 3574 We wwe 5072 dom cdm 5114 ↾ cres 5116 Predcpred 5679 Fun wfun 5882 Fn wfn 5883 ‘cfv 5888

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-iota 5851 df-fun 5890 df-fn 5891 df-fv 5896

This theorem is referenced by: wfrlem5 7419

W3C validator