frrlem8

Description: Lemma for well-founded recursion. dom F is closed under predecessor classes. (Contributed by Scott Fenton, 6-Dec-2022)

	Ref	Expression
Hypotheses	frrlem5.1	$⊢ B = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
	frrlem5.2	$⊢ F = frecs (R, A, G)$
Assertion	frrlem8	$⊢ z \in dom F \to Pred (R, A, z) \subseteq dom F$

Proof

Step	Hyp	Ref	Expression
1		frrlem5.1	$⊢ B = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
2		frrlem5.2	$⊢ F = frecs (R, A, G)$
3		vex	$⊢ z \in V$
4	3	eldm2	$⊢ z \in dom F \leftrightarrow \exists w ⟨z, w⟩ \in F$
5	1 2	frrlem5	$⊢ F = ⋃ B$
6	1	frrlem1	$⊢ B = \{g \| \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))\}$
7	6	unieqi	$⊢ ⋃ B = ⋃ \{g \| \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))\}$
8	5 7	eqtri	$⊢ F = ⋃ \{g \| \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))\}$
9	8	eleq2i	$⊢ ⟨z, w⟩ \in F \leftrightarrow ⟨z, w⟩ \in ⋃ \{g \| \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))\}$
10		eluniab	$⊢ ⟨z, w⟩ \in ⋃ \{g \| \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))\} \leftrightarrow \exists g (⟨z, w⟩ \in g \land \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)})))$
11	9 10	bitri	$⊢ ⟨z, w⟩ \in F \leftrightarrow \exists g (⟨z, w⟩ \in g \land \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)})))$
12		simpr2r	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to \forall z \in a Pred (R, A, z) \subseteq a$
13		vex	$⊢ w \in V$
14	3 13	opeldm	$⊢ ⟨z, w⟩ \in g \to z \in dom g$
15	14	adantr	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to z \in dom g$
16		simpr1	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to g Fn a$
17	16	fndmd	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to dom g = a$
18	15 17	eleqtrd	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to z \in a$
19		rsp	$⊢ \forall z \in a Pred (R, A, z) \subseteq a \to (z \in a \to Pred (R, A, z) \subseteq a)$
20	12 18 19	sylc	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to Pred (R, A, z) \subseteq a$
21	20 17	sseqtrrd	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to Pred (R, A, z) \subseteq dom g$
22		19.8a	$⊢ (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)})) \to \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))$
23	6	eqabri	$⊢ g \in B \leftrightarrow \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))$
24	22 23	sylibr	$⊢ (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)})) \to g \in B$
25	24	adantl	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to g \in B$
26		elssuni	$⊢ g \in B \to g \subseteq ⋃ B$
27	25 26	syl	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to g \subseteq ⋃ B$
28	27 5	sseqtrrdi	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to g \subseteq F$
29		dmss	$⊢ g \subseteq F \to dom g \subseteq dom F$
30	28 29	syl	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to dom g \subseteq dom F$
31	21 30	sstrd	$⊢ (⟨z, w⟩ \in g \land (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to Pred (R, A, z) \subseteq dom F$
32	31	expcom	$⊢ (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)})) \to (⟨z, w⟩ \in g \to Pred (R, A, z) \subseteq dom F)$
33	32	exlimiv	$⊢ \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)})) \to (⟨z, w⟩ \in g \to Pred (R, A, z) \subseteq dom F)$
34	33	impcom	$⊢ (⟨z, w⟩ \in g \land \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to Pred (R, A, z) \subseteq dom F$
35	34	exlimiv	$⊢ \exists g (⟨z, w⟩ \in g \land \exists a (g Fn a \land (a \subseteq A \land \forall z \in a Pred (R, A, z) \subseteq a) \land \forall z \in a g (z) = z G ({g ↾}_{Pred (R, A, z)}))) \to Pred (R, A, z) \subseteq dom F$
36	11 35	sylbi	$⊢ ⟨z, w⟩ \in F \to Pred (R, A, z) \subseteq dom F$
37	36	exlimiv	$⊢ \exists w ⟨z, w⟩ \in F \to Pred (R, A, z) \subseteq dom F$
38	4 37	sylbi	$⊢ z \in dom F \to Pred (R, A, z) \subseteq dom F$

Metamath Proof Explorer

Theorem frrlem8

Proof