onvf1odlem3

Description: Lemma for onvf1od . The value of F at an ordinal A . (Contributed by BTernaryTau, 2-Dec-2025)

	Ref	Expression
Hypotheses	onvf1odlem3.1	$⊢ M = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in ran w\}$
	onvf1odlem3.2	$⊢ N = G (R_{1} (M) ∖ ran w)$
	onvf1odlem3.3	$⊢ F = recs ((w \in V ⟼ N))$
	onvf1odlem3.4	$⊢ B = ⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [A]\}$
	onvf1odlem3.5	$⊢ C = G (R_{1} (B) ∖ F [A])$
Assertion	onvf1odlem3	$⊢ A \in On \to F (A) = C$

Proof

Step	Hyp	Ref	Expression
1		onvf1odlem3.1	$⊢ M = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in ran w\}$
2		onvf1odlem3.2	$⊢ N = G (R_{1} (M) ∖ ran w)$
3		onvf1odlem3.3	$⊢ F = recs ((w \in V ⟼ N))$
4		onvf1odlem3.4	$⊢ B = ⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [A]\}$
5		onvf1odlem3.5	$⊢ C = G (R_{1} (B) ∖ F [A])$
6	3	tfr2	$⊢ A \in On \to F (A) = (w \in V ⟼ N) ({F ↾}_{A})$
7	3	tfr1	$⊢ F Fn On$
8		fnfun	$⊢ F Fn On \to Fun F$
9	7 8	ax-mp	$⊢ Fun F$
10		resfunexg	$⊢ (Fun F \land A \in On) \to {F ↾}_{A} \in V$
11	9 10	mpan	$⊢ A \in On \to {F ↾}_{A} \in V$
12		eleq1w	$⊢ t = v \to (t \in ran r \leftrightarrow v \in ran r)$
13	12	notbid	$⊢ t = v \to (\neg t \in ran r \leftrightarrow \neg v \in ran r)$
14	13	adantl	$⊢ (s = u \land t = v) \to (\neg t \in ran r \leftrightarrow \neg v \in ran r)$
15		fveq2	$⊢ s = u \to R_{1} (s) = R_{1} (u)$
16	15	adantr	$⊢ (s = u \land t = v) \to R_{1} (s) = R_{1} (u)$
17	14 16	cbvrexdva2	$⊢ s = u \to (\exists t \in R_{1} (s) \neg t \in ran r \leftrightarrow \exists v \in R_{1} (u) \neg v \in ran r)$
18	17	cbvrabv	$⊢ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\} = \{u \in On \| \exists v \in R_{1} (u) \neg v \in ran r\}$
19		rneq	$⊢ r = {F ↾}_{A} \to ran r = ran ({F ↾}_{A})$
20		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
21	19 20	eqtr4di	$⊢ r = {F ↾}_{A} \to ran r = F [A]$
22	21	eleq2d	$⊢ r = {F ↾}_{A} \to (v \in ran r \leftrightarrow v \in F [A])$
23	22	notbid	$⊢ r = {F ↾}_{A} \to (\neg v \in ran r \leftrightarrow \neg v \in F [A])$
24	23	rexbidv	$⊢ r = {F ↾}_{A} \to (\exists v \in R_{1} (u) \neg v \in ran r \leftrightarrow \exists v \in R_{1} (u) \neg v \in F [A])$
25	24	rabbidv	$⊢ r = {F ↾}_{A} \to \{u \in On \| \exists v \in R_{1} (u) \neg v \in ran r\} = \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [A]\}$
26	18 25	eqtrid	$⊢ r = {F ↾}_{A} \to \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\} = \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [A]\}$
27	26	inteqd	$⊢ r = {F ↾}_{A} \to ⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\} = ⋂ \{u \in On \| \exists v \in R_{1} (u) \neg v \in F [A]\}$
28	27 4	eqtr4di	$⊢ r = {F ↾}_{A} \to ⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\} = B$
29	28	fveq2d	$⊢ r = {F ↾}_{A} \to R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}) = R_{1} (B)$
30	29 21	difeq12d	$⊢ r = {F ↾}_{A} \to R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}) ∖ ran r = R_{1} (B) ∖ F [A]$
31	30	fveq2d	$⊢ r = {F ↾}_{A} \to G (R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}) ∖ ran r) = G (R_{1} (B) ∖ F [A])$
32	31 5	eqtr4di	$⊢ r = {F ↾}_{A} \to G (R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}) ∖ ran r) = C$
33		eleq1w	$⊢ y = t \to (y \in ran w \leftrightarrow t \in ran w)$
34	33	notbid	$⊢ y = t \to (\neg y \in ran w \leftrightarrow \neg t \in ran w)$
35	34	adantl	$⊢ (x = s \land y = t) \to (\neg y \in ran w \leftrightarrow \neg t \in ran w)$
36		fveq2	$⊢ x = s \to R_{1} (x) = R_{1} (s)$
37	36	adantr	$⊢ (x = s \land y = t) \to R_{1} (x) = R_{1} (s)$
38	35 37	cbvrexdva2	$⊢ x = s \to (\exists y \in R_{1} (x) \neg y \in ran w \leftrightarrow \exists t \in R_{1} (s) \neg t \in ran w)$
39	38	cbvrabv	$⊢ \{x \in On \| \exists y \in R_{1} (x) \neg y \in ran w\} = \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran w\}$
40		rneq	$⊢ w = r \to ran w = ran r$
41	40	eleq2d	$⊢ w = r \to (t \in ran w \leftrightarrow t \in ran r)$
42	41	notbid	$⊢ w = r \to (\neg t \in ran w \leftrightarrow \neg t \in ran r)$
43	42	rexbidv	$⊢ w = r \to (\exists t \in R_{1} (s) \neg t \in ran w \leftrightarrow \exists t \in R_{1} (s) \neg t \in ran r)$
44	43	rabbidv	$⊢ w = r \to \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran w\} = \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}$
45	39 44	eqtrid	$⊢ w = r \to \{x \in On \| \exists y \in R_{1} (x) \neg y \in ran w\} = \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}$
46	45	inteqd	$⊢ w = r \to ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in ran w\} = ⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}$
47	1 46	eqtrid	$⊢ w = r \to M = ⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}$
48	47	fveq2d	$⊢ w = r \to R_{1} (M) = R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\})$
49	48 40	difeq12d	$⊢ w = r \to R_{1} (M) ∖ ran w = R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}) ∖ ran r$
50	49	fveq2d	$⊢ w = r \to G (R_{1} (M) ∖ ran w) = G (R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}) ∖ ran r)$
51	2 50	eqtrid	$⊢ w = r \to N = G (R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}) ∖ ran r)$
52	51	cbvmptv	$⊢ (w \in V ⟼ N) = (r \in V ⟼ G (R_{1} (⋂ \{s \in On \| \exists t \in R_{1} (s) \neg t \in ran r\}) ∖ ran r))$
53	5	fvexi	$⊢ C \in V$
54	32 52 53	fvmpt	$⊢ {F ↾}_{A} \in V \to (w \in V ⟼ N) ({F ↾}_{A}) = C$
55	11 54	syl	$⊢ A \in On \to (w \in V ⟼ N) ({F ↾}_{A}) = C$
56	6 55	eqtrd	$⊢ A \in On \to F (A) = C$

Metamath Proof Explorer

Theorem onvf1odlem3

Proof