wfrlem4OLD - Metamath Proof Explorer

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

Theorem wfrlem4OLD 8258

Description: Lemma for well-ordered recursion. Properties of the restriction of an acceptable function to the domain of another one. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by AV, 18-Jul-2022.)

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

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

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

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

Step	Hyp	Ref	Expression
1		wfrlem4OLD.2	. . . . . 6 ⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2	1	wfrlem2OLD 8255	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔)
3	2	funfnd 6532	. . . 4 ⊢ (𝑔 ∈ 𝐵 → 𝑔 Fn dom 𝑔)
4		fnresin1 6626	. . . 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	wfrlem1OLD 8254	. . . . . . . 8 ⊢ 𝐵 = {𝑔 ∣ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))}
8	7	eqabi 2881	. . . . . . 7 ⊢ (𝑔 ∈ 𝐵 ↔ ∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
9		fndm 6605	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑏 → dom 𝑔 = 𝑏)
10	9	raleqdv 3313	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑏 → (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ↔ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
11	10	biimpar 478	. . . . . . . . . 10 ⊢ ((𝑔 Fn 𝑏 ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → ∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
12		rsp 3230	. . . . . . . . . 10 ⊢ (∀𝑎 ∈ dom 𝑔(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
13	11, 12	syl 17	. . . . . . . . 9 ⊢ ((𝑔 Fn 𝑏 ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) → (𝑎 ∈ dom 𝑔 → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))))
14	13	3adant2 1131	. . . . . . . 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 4155	. . . . . 6 ⊢ (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → 𝑎 ∈ dom 𝑔)
18	16, 17	impel 506	. . . . 5 ⊢ ((𝑔 ∈ 𝐵 ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
19	18	adantlr 713	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
20		fvres 6861	. . . . 5 ⊢ (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑔‘𝑎))
21	20	adantl 482	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑔‘𝑎))
22		resres 5950	. . . . . 6 ⊢ ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)))
23		predss 6261	. . . . . . . . 9 ⊢ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)
24		sseqin2 4175	. . . . . . . . 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	wfrlem1OLD 8254	. . . . . . . . . . . 12 ⊢ 𝐵 = {ℎ ∣ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))}
27	26	eqabi 2881	. . . . . . . . . . 11 ⊢ (ℎ ∈ 𝐵 ↔ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎)))))
28		3an6 1446	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ ((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
29	28	2exbii 1851	. . . . . . . . . . . . 13 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ ∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
30		exdistrv 1959	. . . . . . . . . . . . 13 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ (ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
31	29, 30	bitri 274	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) ↔ (∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))))
32		ssinss1 4197	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ⊆ 𝐴 → (𝑏 ∩ 𝑐) ⊆ 𝐴)
33	32	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → (𝑏 ∩ 𝑐) ⊆ 𝐴)
34		nfra1 3267	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏
35		nfra1 3267	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐
36	34, 35	nfan 1902	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎(∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)
37		elinel1 4155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑏)
38		rsp 3230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → (𝑎 ∈ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
39	37, 38	syl5com 31	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏))
40		elinel2 4156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → 𝑎 ∈ 𝑐)
41		rsp 3230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → (𝑎 ∈ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
42	40, 41	syl5com 31	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → (∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))
43	39, 42	anim12d 609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (𝑏 ∩ 𝑐) → ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)))
44		ssin 4190	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
45	44	biimpi 215	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
46	43, 45	syl6com 37	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → (𝑎 ∈ (𝑏 ∩ 𝑐) → Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
47	36, 46	ralrimi 3240	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
48	47	ad2ant2l 744	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))
49	33, 48	jca 512	. . . . . . . . . . . . . . . 16 ⊢ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
50		fndm 6605	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ Fn 𝑐 → dom ℎ = 𝑐)
51	9, 50	ineqan12d 4174	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) → (dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐))
52		sseq1 3969	. . . . . . . . . . . . . . . . . . 19 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ↔ (𝑏 ∩ 𝑐) ⊆ 𝐴))
53		sseq2 3970	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
54	53	raleqbi1dv 3307	. . . . . . . . . . . . . . . . . . 19 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ) ↔ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))
55	52, 54	anbi12d 631	. . . . . . . . . . . . . . . . . 18 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) ↔ ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐))))
56	55	imbi2d 340	. . . . . . . . . . . . . . . . 17 ⊢ ((dom 𝑔 ∩ dom ℎ) = (𝑏 ∩ 𝑐) → ((((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ))) ↔ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))))
57	51, 56	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) → ((((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ))) ↔ (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((𝑏 ∩ 𝑐) ⊆ 𝐴 ∧ ∀𝑎 ∈ (𝑏 ∩ 𝑐)Pred(𝑅, 𝐴, 𝑎) ⊆ (𝑏 ∩ 𝑐)))))
58	49, 57	mpbiri 257	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) → (((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ))))
59	58	imp 407	. . . . . . . . . . . . . 14 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
60	59	3adant3 1132	. . . . . . . . . . . . 13 ⊢ (((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
61	60	exlimivv 1935	. . . . . . . . . . . 12 ⊢ (∃𝑏∃𝑐((𝑔 Fn 𝑏 ∧ ℎ Fn 𝑐) ∧ ((𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐)) ∧ (∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
62	31, 61	sylbir 234	. . . . . . . . . . 11 ⊢ ((∃𝑏(𝑔 Fn 𝑏 ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑏) ∧ ∀𝑎 ∈ 𝑏 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))) ∧ ∃𝑐(ℎ Fn 𝑐 ∧ (𝑐 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝑐 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝑐) ∧ ∀𝑎 ∈ 𝑐 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ Pred(𝑅, 𝐴, 𝑎))))) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
63	8, 27, 62	syl2anb 598	. . . . . . . . . 10 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
64	63	adantr 481	. . . . . . . . 9 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)))
65		simpr 485	. . . . . . . . 9 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → 𝑎 ∈ (dom 𝑔 ∩ dom ℎ))
66		preddowncl 6286	. . . . . . . . 9 ⊢ (((dom 𝑔 ∩ dom ℎ) ⊆ 𝐴 ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)Pred(𝑅, 𝐴, 𝑎) ⊆ (dom 𝑔 ∩ dom ℎ)) → (𝑎 ∈ (dom 𝑔 ∩ dom ℎ) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, 𝐴, 𝑎)))
67	64, 65, 66	sylc 65	. . . . . . . 8 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎) = Pred(𝑅, 𝐴, 𝑎))
68	25, 67	eqtrid 2788	. . . . . . 7 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = Pred(𝑅, 𝐴, 𝑎))
69	68	reseq2d 5937	. . . . . 6 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝑔 ↾ ((dom 𝑔 ∩ dom ℎ) ∩ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
70	22, 69	eqtrid 2788	. . . . 5 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑎)))
71	70	fveq2d 6846	. . . 4 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))) = (𝐹‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑎))))
72	19, 21, 71	3eqtr4d 2786	. . 3 ⊢ (((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) ∧ 𝑎 ∈ (dom 𝑔 ∩ dom ℎ)) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
73	72	ralrimiva 3143	. 2 ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝐹‘((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))
74	6, 73	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 1087 = wceq 1541 ∃wex 1781 ∈ wcel 2106 {cab 2713 ∀wral 3064 ∩ cin 3909 ⊆ wss 3910 dom cdm 5633 ↾ cres 5635 Predcpred 6252 Fn wfn 6491 ‘cfv 6496

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-iota 6448 df-fun 6498 df-fn 6499 df-fv 6504

This theorem is referenced by: wfrlem5OLD 8259

W3C validator