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 7305

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 7302	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔)
3		funfn 5833	. . . . 5 ⊢ (Fun 𝑔 ↔ 𝑔 Fn dom 𝑔)
4	2, 3	sylib 207	. . . 4 ⊢ (𝑔 ∈ 𝐵 → 𝑔 Fn dom 𝑔)
5		fnresin1 5919	. . . 4 ⊢ (𝑔 Fn dom 𝑔 → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
6	4, 5	syl 17	. . 3 ⊢ (𝑔 ∈ 𝐵 → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
7	6	adantr 480	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ))
8		inss1 3795	. . . . . . . 8 ⊢ (dom 𝑔 ∩ dom ℎ) ⊆ dom 𝑔
9	8	sseli 3564	. . . . . . 7 ⊢ (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → 𝑎 ∈ dom 𝑔)
10	1	wfrlem1 7301	. . . . . . . . 9 ⊢ 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))}
11	10	abeq2i 2722	. . . . . . . 8 ⊢ (𝑔 ∈ 𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
12		fndm 5904	. . . . . . . . . . . . 13 ⊢ (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
13	12	raleqdv 3121	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑏 → (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ↔ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
14	13	biimpar 501	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑏 ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
15		rsp 2913	. . . . . . . . . . 11 ⊢ (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝑔 Fn 𝑏 ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
17	16	3adant2 1073	. . . . . . . . 9 ⊢ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
18	17	exlimiv 1845	. . . . . . . 8 ⊢ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
19	11, 18	sylbi 206	. . . . . . 7 ⊢ (𝑔 ∈ 𝐵 → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
20	9, 19	syl5 33	. . . . . 6 ⊢ (𝑔 ∈ 𝐵 → (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
21	20	imp 444	. . . . 5 ⊢ ((𝑔 ∈ 𝐵 ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
22	21	adantlr 747	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
23		fvres 6117	. . . . 5 ⊢ (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑔‘𝑎))
24	23	adantl 481	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑔‘𝑎))
25		resres 5329	. . . . . 6 ⊢ ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))
26		predss 5604	. . . . . . . . 9 ⊢ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)
27		sseqin2 3779	. . . . . . . . 9 ⊢ (Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))
28	26, 27	mpbi 219	. . . . . . . 8 ⊢ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)
29	1	wfrlem1 7301	. . . . . . . . . . . 12 ⊢ 𝐵 = {ℎ ∣ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))}
30	29	abeq2i 2722	. . . . . . . . . . 11 ⊢ (ℎ ∈ 𝐵 ↔ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎)))))
31		3an6 1401	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
32	31	2exbii 1765	. . . . . . . . . . . . 13 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ ∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
33		eeanv 2170	. . . . . . . . . . . . 13 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
34	32, 33	bitri 263	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
35		ssinss1 3803	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ⊆ 𝐴 → (𝑏 ∩ 𝑐) ⊆ 𝐴)
36	35	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → (𝑏 ∩ 𝑐) ⊆ 𝐴)
37		nfra1 2925	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
38		nfra1 2925	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
39	37, 38	nfan 1816	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎(∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
40		inss1 3795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∩ 𝑐) ⊆ 𝑏
41	40	sseli 3564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑏)
42		rsp 2913	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎 ∈ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
43	41, 42	syl5com 31	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
44		inss2 3796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∩ 𝑐) ⊆ 𝑐
45	44	sseli 3564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑐)
46		rsp 2913	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎 ∈ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
47	45, 46	syl5com 31	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
48	43, 47	anim12d 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
49		ssin 3797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
50	49	biimpi 205	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
51	48, 50	syl6com 36	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (𝑎 ∈ (𝑏 ∩ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
52	39, 51	ralrimi 2940	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
53	52	ad2ant2l 778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
54	36, 53	jca 553	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
55		fndm 5904	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ Fn 𝑐 → dom ℎ = 𝑐)
56	12, 55	ineqan12d 3778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) → (dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐))
57		sseq1 3589	. . . . . . . . . . . . . . . . . . 19 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ↔ (𝑏 ∩ 𝑐) ⊆ 𝐴))
58		sseq2 3590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
59	58	raleqbi1dv 3123	. . . . . . . . . . . . . . . . . . 19 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
60	57, 59	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) ↔ ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))))
61	60	imbi2d 329	. . . . . . . . . . . . . . . . 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 247	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) → (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ))))
64	63	imp 444	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
65	64	3adant3 1074	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
66	65	exlimivv 1847	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
67	34, 66	sylbir 224	. . . . . . . . . . 11 ⊢ ((∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
68	11, 30, 67	syl2anb 495	. . . . . . . . . 10 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
69	68	adantr 480	. . . . . . . . 9 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
70		simpr 476	. . . . . . . . 9 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → 𝑎 ∈ (dom 𝑔 ∩ dom ℎ))
71		preddowncl 5624	. . . . . . . . 9 ⊢ (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) → (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, 𝐴, 𝑎)))
72	69, 70, 71	sylc 63	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, 𝐴, 𝑎))
73	28, 72	syl5eq 2656	. . . . . . 7 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
74	73	reseq2d 5317	. . . . . 6 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
75	25, 74	syl5eq 2656	. . . . 5 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
76	75	fveq2d 6107	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
77	22, 24, 76	3eqtr4d 2654	. . 3 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
78	77	ralrimiva 2949	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
79	7, 78	jca 553	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 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ∀wral 2896 ∩ cin 3539 ⊆ wss 3540 We wwe 4996 dom cdm 5038 ↾ cres 5040 Predcpred 5596 Fun wfun 5798 Fn wfn 5799 ‘cfv 5804

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-iota 5768 df-fun 5806 df-fn 5807 df-fv 5812

This theorem is referenced by: wfrlem5 7306

W3C validator