frrlem12

Description: Lemma for well-founded recursion. Next, we calculate the value of C . (Contributed by Scott Fenton, 7-Dec-2022)

	Ref	Expression
Hypotheses	frrlem11.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)}))\}$
	frrlem11.2	$⊢ F = frecs (R, A, G)$
	frrlem11.3	$⊢ (φ \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)$
	frrlem11.4	$⊢ C = ({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
	frrlem12.5	$⊢ φ \to R Fr A$
	frrlem12.6	$⊢ (φ \land z \in A) \to Pred (R, A, z) \subseteq S$
	frrlem12.7	$⊢ (φ \land z \in A) \to \forall w \in S Pred (R, A, w) \subseteq S$
Assertion	frrlem12	$⊢ (φ \land z \in (A ∖ dom F) \land w \in ((S \cap dom F) \cup \{z\})) \to C (w) = w G ({C ↾}_{Pred (R, A, w)})$

Proof

Step	Hyp	Ref	Expression
1		frrlem11.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		frrlem11.2	$⊢ F = frecs (R, A, G)$
3		frrlem11.3	$⊢ (φ \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)$
4		frrlem11.4	$⊢ C = ({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
5		frrlem12.5	$⊢ φ \to R Fr A$
6		frrlem12.6	$⊢ (φ \land z \in A) \to Pred (R, A, z) \subseteq S$
7		frrlem12.7	$⊢ (φ \land z \in A) \to \forall w \in S Pred (R, A, w) \subseteq S$
8		elun	$⊢ w \in ((S \cap dom F) \cup \{z\}) \leftrightarrow (w \in (S \cap dom F) \lor w \in \{z\})$
9		velsn	$⊢ w \in \{z\} \leftrightarrow w = z$
10	9	orbi2i	$⊢ (w \in (S \cap dom F) \lor w \in \{z\}) \leftrightarrow (w \in (S \cap dom F) \lor w = z)$
11	8 10	bitri	$⊢ w \in ((S \cap dom F) \cup \{z\}) \leftrightarrow (w \in (S \cap dom F) \lor w = z)$
12		elinel2	$⊢ w \in (S \cap dom F) \to w \in dom F$
13	1	frrlem1	$⊢ B = \{p \| \exists q (p Fn q \land (q \subseteq A \land \forall w \in q Pred (R, A, w) \subseteq q) \land \forall w \in q p (w) = w G ({p ↾}_{Pred (R, A, w)}))\}$
14		breq1	$⊢ x = q \to (x g u \leftrightarrow q g u)$
15		breq1	$⊢ x = q \to (x h v \leftrightarrow q h v)$
16	14 15	anbi12d	$⊢ x = q \to ((x g u \land x h v) \leftrightarrow (q g u \land q h v))$
17	16	imbi1d	$⊢ x = q \to (((x g u \land x h v) \to u = v) \leftrightarrow ((q g u \land q h v) \to u = v))$
18	17	imbi2d	$⊢ x = q \to (((φ \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)) \leftrightarrow ((φ \land (g \in B \land h \in B)) \to ((q g u \land q h v) \to u = v)))$
19	18 3	chvarvv	$⊢ (φ \land (g \in B \land h \in B)) \to ((q g u \land q h v) \to u = v)$
20	13 2 19	frrlem10	$⊢ (φ \land w \in dom F) \to F (w) = w G ({F ↾}_{Pred (R, A, w)})$
21	12 20	sylan2	$⊢ (φ \land w \in (S \cap dom F)) \to F (w) = w G ({F ↾}_{Pred (R, A, w)})$
22	21	adantlr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to F (w) = w G ({F ↾}_{Pred (R, A, w)})$
23	4	fveq1i	$⊢ C (w) = (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) (w)$
24	1 2 3	frrlem9	$⊢ φ \to Fun F$
25	24	funresd	$⊢ φ \to Fun ({F ↾}_{S})$
26		dmres	$⊢ dom ({F ↾}_{S}) = S \cap dom F$
27		df-fn	$⊢ ({F ↾}_{S}) Fn (S \cap dom F) \leftrightarrow (Fun ({F ↾}_{S}) \land dom ({F ↾}_{S}) = S \cap dom F)$
28	25 26 27	sylanblrc	$⊢ φ \to ({F ↾}_{S}) Fn (S \cap dom F)$
29	28	adantr	$⊢ (φ \land z \in (A ∖ dom F)) \to ({F ↾}_{S}) Fn (S \cap dom F)$
30	29	adantr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to ({F ↾}_{S}) Fn (S \cap dom F)$
31		vex	$⊢ z \in V$
32		ovex	$⊢ z G ({F ↾}_{Pred (R, A, z)}) \in V$
33	31 32	fnsn	$⊢ \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\}$
34	33	a1i	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\}$
35		eldifn	$⊢ z \in (A ∖ dom F) \to \neg z \in dom F$
36		elinel2	$⊢ z \in (S \cap dom F) \to z \in dom F$
37	35 36	nsyl	$⊢ z \in (A ∖ dom F) \to \neg z \in (S \cap dom F)$
38		disjsn	$⊢ (S \cap dom F) \cap \{z\} = \emptyset \leftrightarrow \neg z \in (S \cap dom F)$
39	37 38	sylibr	$⊢ z \in (A ∖ dom F) \to (S \cap dom F) \cap \{z\} = \emptyset$
40	39	adantl	$⊢ (φ \land z \in (A ∖ dom F)) \to (S \cap dom F) \cap \{z\} = \emptyset$
41	40	adantr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to (S \cap dom F) \cap \{z\} = \emptyset$
42		simpr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to w \in (S \cap dom F)$
43		fvun1	$⊢ (({F ↾}_{S}) Fn (S \cap dom F) \land \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\} \land ((S \cap dom F) \cap \{z\} = \emptyset \land w \in (S \cap dom F))) \to (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) (w) = ({F ↾}_{S}) (w)$
44	30 34 41 42 43	syl112anc	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) (w) = ({F ↾}_{S}) (w)$
45	23 44	eqtrid	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to C (w) = ({F ↾}_{S}) (w)$
46		elinel1	$⊢ w \in (S \cap dom F) \to w \in S$
47	46	adantl	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to w \in S$
48	47	fvresd	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to ({F ↾}_{S}) (w) = F (w)$
49	45 48	eqtrd	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to C (w) = F (w)$
50	1 2 3 4	frrlem11	$⊢ (φ \land z \in (A ∖ dom F)) \to C Fn ((S \cap dom F) \cup \{z\})$
51		fnfun	$⊢ C Fn ((S \cap dom F) \cup \{z\}) \to Fun C$
52	50 51	syl	$⊢ (φ \land z \in (A ∖ dom F)) \to Fun C$
53	52	adantr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Fun C$
54		ssun1	$⊢ {F ↾}_{S} \subseteq ({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
55	54 4	sseqtrri	$⊢ {F ↾}_{S} \subseteq C$
56	55	a1i	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to {F ↾}_{S} \subseteq C$
57		eldifi	$⊢ z \in (A ∖ dom F) \to z \in A$
58	57 7	sylan2	$⊢ (φ \land z \in (A ∖ dom F)) \to \forall w \in S Pred (R, A, w) \subseteq S$
59		rspa	$⊢ (\forall w \in S Pred (R, A, w) \subseteq S \land w \in S) \to Pred (R, A, w) \subseteq S$
60	58 46 59	syl2an	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Pred (R, A, w) \subseteq S$
61	1 2	frrlem8	$⊢ w \in dom F \to Pred (R, A, w) \subseteq dom F$
62	12 61	syl	$⊢ w \in (S \cap dom F) \to Pred (R, A, w) \subseteq dom F$
63	62	adantl	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Pred (R, A, w) \subseteq dom F$
64	60 63	ssind	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Pred (R, A, w) \subseteq S \cap dom F$
65	64 26	sseqtrrdi	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Pred (R, A, w) \subseteq dom ({F ↾}_{S})$
66		fun2ssres	$⊢ (Fun C \land {F ↾}_{S} \subseteq C \land Pred (R, A, w) \subseteq dom ({F ↾}_{S})) \to {C ↾}_{Pred (R, A, w)} = {({F ↾}_{S}) ↾}_{Pred (R, A, w)}$
67	53 56 65 66	syl3anc	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to {C ↾}_{Pred (R, A, w)} = {({F ↾}_{S}) ↾}_{Pred (R, A, w)}$
68	60	resabs1d	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to {({F ↾}_{S}) ↾}_{Pred (R, A, w)} = {F ↾}_{Pred (R, A, w)}$
69	67 68	eqtrd	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to {C ↾}_{Pred (R, A, w)} = {F ↾}_{Pred (R, A, w)}$
70	69	oveq2d	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to w G ({C ↾}_{Pred (R, A, w)}) = w G ({F ↾}_{Pred (R, A, w)})$
71	22 49 70	3eqtr4d	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to C (w) = w G ({C ↾}_{Pred (R, A, w)})$
72	71	ex	$⊢ (φ \land z \in (A ∖ dom F)) \to (w \in (S \cap dom F) \to C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
73	31 32	fvsn	$⊢ \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} (z) = z G ({F ↾}_{Pred (R, A, z)})$
74	4	fveq1i	$⊢ C (z) = (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) (z)$
75	33	a1i	$⊢ (φ \land z \in (A ∖ dom F)) \to \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\}$
76		vsnid	$⊢ z \in \{z\}$
77	76	a1i	$⊢ (φ \land z \in (A ∖ dom F)) \to z \in \{z\}$
78		fvun2	$⊢ (({F ↾}_{S}) Fn (S \cap dom F) \land \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\} \land ((S \cap dom F) \cap \{z\} = \emptyset \land z \in \{z\})) \to (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) (z) = \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} (z)$
79	29 75 40 77 78	syl112anc	$⊢ (φ \land z \in (A ∖ dom F)) \to (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) (z) = \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} (z)$
80	74 79	eqtrid	$⊢ (φ \land z \in (A ∖ dom F)) \to C (z) = \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} (z)$
81	4	reseq1i	$⊢ {C ↾}_{Pred (R, A, z)} = {(({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) ↾}_{Pred (R, A, z)}$
82		resundir	$⊢ {(({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) ↾}_{Pred (R, A, z)} = ({({F ↾}_{S}) ↾}_{Pred (R, A, z)}) \cup ({\{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)})$
83	81 82	eqtri	$⊢ {C ↾}_{Pred (R, A, z)} = ({({F ↾}_{S}) ↾}_{Pred (R, A, z)}) \cup ({\{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)})$
84	57 6	sylan2	$⊢ (φ \land z \in (A ∖ dom F)) \to Pred (R, A, z) \subseteq S$
85	84	resabs1d	$⊢ (φ \land z \in (A ∖ dom F)) \to {({F ↾}_{S}) ↾}_{Pred (R, A, z)} = {F ↾}_{Pred (R, A, z)}$
86		predfrirr	$⊢ R Fr A \to \neg z \in Pred (R, A, z)$
87	5 86	syl	$⊢ φ \to \neg z \in Pred (R, A, z)$
88	87	adantr	$⊢ (φ \land z \in (A ∖ dom F)) \to \neg z \in Pred (R, A, z)$
89		ressnop0	$⊢ \neg z \in Pred (R, A, z) \to {\{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)} = \emptyset$
90	88 89	syl	$⊢ (φ \land z \in (A ∖ dom F)) \to {\{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)} = \emptyset$
91	85 90	uneq12d	$⊢ (φ \land z \in (A ∖ dom F)) \to ({({F ↾}_{S}) ↾}_{Pred (R, A, z)}) \cup ({\{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)}) = ({F ↾}_{Pred (R, A, z)}) \cup \emptyset$
92		un0	$⊢ ({F ↾}_{Pred (R, A, z)}) \cup \emptyset = {F ↾}_{Pred (R, A, z)}$
93	91 92	eqtrdi	$⊢ (φ \land z \in (A ∖ dom F)) \to ({({F ↾}_{S}) ↾}_{Pred (R, A, z)}) \cup ({\{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)}) = {F ↾}_{Pred (R, A, z)}$
94	83 93	eqtrid	$⊢ (φ \land z \in (A ∖ dom F)) \to {C ↾}_{Pred (R, A, z)} = {F ↾}_{Pred (R, A, z)}$
95	94	oveq2d	$⊢ (φ \land z \in (A ∖ dom F)) \to z G ({C ↾}_{Pred (R, A, z)}) = z G ({F ↾}_{Pred (R, A, z)})$
96	73 80 95	3eqtr4a	$⊢ (φ \land z \in (A ∖ dom F)) \to C (z) = z G ({C ↾}_{Pred (R, A, z)})$
97		fveq2	$⊢ w = z \to C (w) = C (z)$
98		id	$⊢ w = z \to w = z$
99		predeq3	$⊢ w = z \to Pred (R, A, w) = Pred (R, A, z)$
100	99	reseq2d	$⊢ w = z \to {C ↾}_{Pred (R, A, w)} = {C ↾}_{Pred (R, A, z)}$
101	98 100	oveq12d	$⊢ w = z \to w G ({C ↾}_{Pred (R, A, w)}) = z G ({C ↾}_{Pred (R, A, z)})$
102	97 101	eqeq12d	$⊢ w = z \to (C (w) = w G ({C ↾}_{Pred (R, A, w)}) \leftrightarrow C (z) = z G ({C ↾}_{Pred (R, A, z)}))$
103	96 102	syl5ibrcom	$⊢ (φ \land z \in (A ∖ dom F)) \to (w = z \to C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
104	72 103	jaod	$⊢ (φ \land z \in (A ∖ dom F)) \to ((w \in (S \cap dom F) \lor w = z) \to C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
105	11 104	biimtrid	$⊢ (φ \land z \in (A ∖ dom F)) \to (w \in ((S \cap dom F) \cup \{z\}) \to C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
106	105	3impia	$⊢ (φ \land z \in (A ∖ dom F) \land w \in ((S \cap dom F) \cup \{z\})) \to C (w) = w G ({C ↾}_{Pred (R, A, w)})$

Metamath Proof Explorer

Theorem frrlem12

Proof