frrlem12

Description: Lemma for 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		funres	$⊢ Fun F \to Fun ({F ↾}_{S})$
26	24 25	syl	$⊢ φ \to Fun ({F ↾}_{S})$
27		dmres	$⊢ dom ({F ↾}_{S}) = S \cap dom F$
28		df-fn	$⊢ ({F ↾}_{S}) Fn (S \cap dom F) \leftrightarrow (Fun ({F ↾}_{S}) \land dom ({F ↾}_{S}) = S \cap dom F)$
29	26 27 28	sylanblrc	$⊢ φ \to ({F ↾}_{S}) Fn (S \cap dom F)$
30	29	adantr	$⊢ (φ \land z \in (A ∖ dom F)) \to ({F ↾}_{S}) Fn (S \cap dom F)$
31	30	adantr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to ({F ↾}_{S}) Fn (S \cap dom F)$
32		vex	$⊢ z \in V$
33		ovex	$⊢ z G ({F ↾}_{Pred (R, A, z)}) \in V$
34	32 33	fnsn	$⊢ \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\}$
35	34	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\}$
36		eldifn	$⊢ z \in (A ∖ dom F) \to \neg z \in dom F$
37		elinel2	$⊢ z \in (S \cap dom F) \to z \in dom F$
38	36 37	nsyl	$⊢ z \in (A ∖ dom F) \to \neg z \in (S \cap dom F)$
39		disjsn	$⊢ (S \cap dom F) \cap \{z\} = \emptyset \leftrightarrow \neg z \in (S \cap dom F)$
40	38 39	sylibr	$⊢ z \in (A ∖ dom F) \to (S \cap dom F) \cap \{z\} = \emptyset$
41	40	adantl	$⊢ (φ \land z \in (A ∖ dom F)) \to (S \cap dom F) \cap \{z\} = \emptyset$
42	41	adantr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to (S \cap dom F) \cap \{z\} = \emptyset$
43		simpr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to w \in (S \cap dom F)$
44		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)$
45	31 35 42 43 44	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)$
46	23 45	syl5eq	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to C (w) = ({F ↾}_{S}) (w)$
47		elinel1	$⊢ w \in (S \cap dom F) \to w \in S$
48	47	adantl	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to w \in S$
49	48	fvresd	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to ({F ↾}_{S}) (w) = F (w)$
50	46 49	eqtrd	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to C (w) = F (w)$
51	1 2 3 4	frrlem11	$⊢ (φ \land z \in (A ∖ dom F)) \to C Fn ((S \cap dom F) \cup \{z\})$
52		fnfun	$⊢ C Fn ((S \cap dom F) \cup \{z\}) \to Fun C$
53	51 52	syl	$⊢ (φ \land z \in (A ∖ dom F)) \to Fun C$
54	53	adantr	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Fun C$
55		ssun1	$⊢ {F ↾}_{S} \subseteq ({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
56	55 4	sseqtrri	$⊢ {F ↾}_{S} \subseteq C$
57	56	a1i	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to {F ↾}_{S} \subseteq C$
58		eldifi	$⊢ z \in (A ∖ dom F) \to z \in A$
59	58 7	sylan2	$⊢ (φ \land z \in (A ∖ dom F)) \to \forall w \in S Pred (R, A, w) \subseteq S$
60		rspa	$⊢ (\forall w \in S Pred (R, A, w) \subseteq S \land w \in S) \to Pred (R, A, w) \subseteq S$
61	59 47 60	syl2an	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Pred (R, A, w) \subseteq S$
62	1 2	frrlem8	$⊢ w \in dom F \to Pred (R, A, w) \subseteq dom F$
63	12 62	syl	$⊢ w \in (S \cap dom F) \to Pred (R, A, w) \subseteq dom F$
64	63	adantl	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Pred (R, A, w) \subseteq dom F$
65	61 64	ssind	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Pred (R, A, w) \subseteq S \cap dom F$
66	65 27	sseqtrrdi	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to Pred (R, A, w) \subseteq dom ({F ↾}_{S})$
67		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)}$
68	54 57 66 67	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)}$
69	61	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)}$
70	68 69	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)}$
71	70	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)})$
72	22 50 71	3eqtr4d	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in (S \cap dom F)) \to C (w) = w G ({C ↾}_{Pred (R, A, w)})$
73	72	ex	$⊢ (φ \land z \in (A ∖ dom F)) \to (w \in (S \cap dom F) \to C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
74	32 33	fvsn	$⊢ \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} (z) = z G ({F ↾}_{Pred (R, A, z)})$
75	4	fveq1i	$⊢ C (z) = (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) (z)$
76	34	a1i	$⊢ (φ \land z \in (A ∖ dom F)) \to \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\}$
77		vsnid	$⊢ z \in \{z\}$
78	77	a1i	$⊢ (φ \land z \in (A ∖ dom F)) \to z \in \{z\}$
79		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)$
80	30 76 41 78 79	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)$
81	75 80	syl5eq	$⊢ (φ \land z \in (A ∖ dom F)) \to C (z) = \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} (z)$
82	4	reseq1i	$⊢ {C ↾}_{Pred (R, A, z)} = {(({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) ↾}_{Pred (R, A, z)}$
83		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)})$
84	82 83	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)})$
85	58 6	sylan2	$⊢ (φ \land z \in (A ∖ dom F)) \to Pred (R, A, z) \subseteq S$
86	85	resabs1d	$⊢ (φ \land z \in (A ∖ dom F)) \to {({F ↾}_{S}) ↾}_{Pred (R, A, z)} = {F ↾}_{Pred (R, A, z)}$
87		predfrirr	$⊢ R Fr A \to \neg z \in Pred (R, A, z)$
88	5 87	syl	$⊢ φ \to \neg z \in Pred (R, A, z)$
89	88	adantr	$⊢ (φ \land z \in (A ∖ dom F)) \to \neg z \in Pred (R, A, z)$
90		ressnop0	$⊢ \neg z \in Pred (R, A, z) \to {\{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)} = \emptyset$
91	89 90	syl	$⊢ (φ \land z \in (A ∖ dom F)) \to {\{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)} = \emptyset$
92	86 91	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$
93		un0	$⊢ ({F ↾}_{Pred (R, A, z)}) \cup \emptyset = {F ↾}_{Pred (R, A, z)}$
94	92 93	syl6eq	$⊢ (φ \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)}$
95	84 94	syl5eq	$⊢ (φ \land z \in (A ∖ dom F)) \to {C ↾}_{Pred (R, A, z)} = {F ↾}_{Pred (R, A, z)}$
96	95	oveq2d	$⊢ (φ \land z \in (A ∖ dom F)) \to z G ({C ↾}_{Pred (R, A, z)}) = z G ({F ↾}_{Pred (R, A, z)})$
97	74 81 96	3eqtr4a	$⊢ (φ \land z \in (A ∖ dom F)) \to C (z) = z G ({C ↾}_{Pred (R, A, z)})$
98		fveq2	$⊢ w = z \to C (w) = C (z)$
99		id	$⊢ w = z \to w = z$
100		predeq3	$⊢ w = z \to Pred (R, A, w) = Pred (R, A, z)$
101	100	reseq2d	$⊢ w = z \to {C ↾}_{Pred (R, A, w)} = {C ↾}_{Pred (R, A, z)}$
102	99 101	oveq12d	$⊢ w = z \to w G ({C ↾}_{Pred (R, A, w)}) = z G ({C ↾}_{Pred (R, A, z)})$
103	98 102	eqeq12d	$⊢ w = z \to (C (w) = w G ({C ↾}_{Pred (R, A, w)}) \leftrightarrow C (z) = z G ({C ↾}_{Pred (R, A, z)}))$
104	97 103	syl5ibrcom	$⊢ (φ \land z \in (A ∖ dom F)) \to (w = z \to C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
105	73 104	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)}))$
106	11 105	syl5bi	$⊢ (φ \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)}))$
107	106	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