finxpreclem4

Description: Lemma for ^^ recursion theorems. (Contributed by ML, 23-Oct-2020)

		Ref	Expression
	Hypothesis	finxpreclem4.1	$⊢ F = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)))$
	Assertion	finxpreclem4	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨N, y⟩) (N) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (⋃ N)$

Proof

Step	Hyp	Ref	Expression
1		finxpreclem4.1	$⊢ F = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)))$
2		2onn	$⊢ 2_{𝑜} \in ω$
3		nnon	$⊢ N \in ω \to N \in On$
4		2on	$⊢ 2_{𝑜} \in On$
5		oawordeu	$⊢ ((2_{𝑜} \in On \land N \in On) \land 2_{𝑜} \subseteq N) \to \exists! o \in On 2_{𝑜} +_{𝑜} o = N$
6	4 5	mpanl1	$⊢ (N \in On \land 2_{𝑜} \subseteq N) \to \exists! o \in On 2_{𝑜} +_{𝑜} o = N$
7		riotasbc	$⊢ \exists! o \in On 2_{𝑜} +_{𝑜} o = N \to \underset{˙}{[} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o \underset{˙}{]} 2_{𝑜} +_{𝑜} o = N$
8	6 7	syl	$⊢ (N \in On \land 2_{𝑜} \subseteq N) \to \underset{˙}{[} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o \underset{˙}{]} 2_{𝑜} +_{𝑜} o = N$
9		riotaex	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in V$
10		sbceq1g	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in V \to (\underset{˙}{[} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o \underset{˙}{]} 2_{𝑜} +_{𝑜} o = N \leftrightarrow ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ (2_{𝑜} +_{𝑜} o) = N)$
11	9 10	ax-mp	$⊢ \underset{˙}{[} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o \underset{˙}{]} 2_{𝑜} +_{𝑜} o = N \leftrightarrow ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ (2_{𝑜} +_{𝑜} o) = N$
12		csbov2g	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in V \to ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ (2_{𝑜} +_{𝑜} o) = 2_{𝑜} +_{𝑜} ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ o$
13	9 12	ax-mp	$⊢ ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ (2_{𝑜} +_{𝑜} o) = 2_{𝑜} +_{𝑜} ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ o$
14	9	csbvargi	$⊢ ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ o = (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)$
15	14	oveq2i	$⊢ 2_{𝑜} +_{𝑜} ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ o = 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)$
16	13 15	eqtri	$⊢ ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ (2_{𝑜} +_{𝑜} o) = 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)$
17	16	eqeq1i	$⊢ ⦋ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o ⦌ (2_{𝑜} +_{𝑜} o) = N \leftrightarrow 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) = N$
18	11 17	bitri	$⊢ \underset{˙}{[} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) / o \underset{˙}{]} 2_{𝑜} +_{𝑜} o = N \leftrightarrow 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) = N$
19	8 18	sylib	$⊢ (N \in On \land 2_{𝑜} \subseteq N) \to 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) = N$
20	3 19	sylan	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) = N$
21		simpl	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to N \in ω$
22	20 21	eqeltrd	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω$
23		riotacl	$⊢ \exists! o \in On 2_{𝑜} +_{𝑜} o = N \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in On$
24		riotaund	$⊢ \neg \exists! o \in On 2_{𝑜} +_{𝑜} o = N \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) = \emptyset$
25		0elon	$⊢ \emptyset \in On$
26	24 25	eqeltrdi	$⊢ \neg \exists! o \in On 2_{𝑜} +_{𝑜} o = N \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in On$
27	23 26	pm2.61i	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in On$
28		nnarcl	$⊢ (2_{𝑜} \in On \land (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in On) \to (2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω \leftrightarrow (2_{𝑜} \in ω \land (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω))$
29	4 28	mpan	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in On \to (2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω \leftrightarrow (2_{𝑜} \in ω \land (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω))$
30	2	biantrur	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω \leftrightarrow (2_{𝑜} \in ω \land (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω)$
31	29 30	bitr4di	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in On \to (2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω \leftrightarrow (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω)$
32	27 31	ax-mp	$⊢ 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω \leftrightarrow (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω$
33	22 32	sylib	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω$
34		nnacom	$⊢ (2_{𝑜} \in ω \land (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω) \to 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) = (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 2_{𝑜}$
35	2 33 34	sylancr	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to 2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) = (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 2_{𝑜}$
36		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
37	36	oveq2i	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 2_{𝑜} = (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} suc 1_{𝑜}$
38		1onn	$⊢ 1_{𝑜} \in ω$
39		nnasuc	$⊢ ((ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω \land 1_{𝑜} \in ω) \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} suc 1_{𝑜} = suc ((ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜})$
40	33 38 39	sylancl	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} suc 1_{𝑜} = suc ((ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜})$
41	37 40	syl5eq	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 2_{𝑜} = suc ((ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜})$
42	35 20 41	3eqtr3d	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to N = suc ((ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜})$
43	3	adantr	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to N \in On$
44		sucidg	$⊢ 1_{𝑜} \in ω \to 1_{𝑜} \in suc 1_{𝑜}$
45	38 44	ax-mp	$⊢ 1_{𝑜} \in suc 1_{𝑜}$
46	45 36	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
47		ssel	$⊢ 2_{𝑜} \subseteq N \to (1_{𝑜} \in 2_{𝑜} \to 1_{𝑜} \in N)$
48	46 47	mpi	$⊢ 2_{𝑜} \subseteq N \to 1_{𝑜} \in N$
49	48	ne0d	$⊢ 2_{𝑜} \subseteq N \to N \neq \emptyset$
50	49	adantl	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to N \neq \emptyset$
51		nnlim	$⊢ N \in ω \to \neg Lim N$
52	51	adantr	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to \neg Lim N$
53		onsucuni3	$⊢ (N \in On \land N \neq \emptyset \land \neg Lim N) \to N = suc ⋃ N$
54	43 50 52 53	syl3anc	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to N = suc ⋃ N$
55		nnacom	$⊢ ((ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω \land 1_{𝑜} \in ω) \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜} = 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)$
56	33 38 55	sylancl	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜} = 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)$
57		suceq	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜} = 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \to suc ((ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜}) = suc (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N))$
58	56 57	syl	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to suc ((ι o \in On \| 2_{𝑜} +_{𝑜} o = N) +_{𝑜} 1_{𝑜}) = suc (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N))$
59	42 54 58	3eqtr3d	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to suc ⋃ N = suc (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N))$
60		ordom	$⊢ Ord ω$
61		ordelss	$⊢ (Ord ω \land N \in ω) \to N \subseteq ω$
62	60 61	mpan	$⊢ N \in ω \to N \subseteq ω$
63		nnfi	$⊢ N \in ω \to N \in Fin$
64		nnunifi	$⊢ (N \subseteq ω \land N \in Fin) \to ⋃ N \in ω$
65	62 63 64	syl2anc	$⊢ N \in ω \to ⋃ N \in ω$
66	65	adantr	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to ⋃ N \in ω$
67		nnacl	$⊢ (1_{𝑜} \in ω \land (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω) \to 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω$
68	38 33 67	sylancr	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω$
69		peano4	$⊢ (⋃ N \in ω \land 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω) \to (suc ⋃ N = suc (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)) \leftrightarrow ⋃ N = 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N))$
70	66 68 69	syl2anc	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to (suc ⋃ N = suc (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)) \leftrightarrow ⋃ N = 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N))$
71	59 70	mpbid	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to ⋃ N = 1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)$
72	71	fveq2d	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to rec (F, ⟨⋃ N, 1^{st} (y)⟩) (⋃ N) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N))$
73	72	adantr	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨⋃ N, 1^{st} (y)⟩) (⋃ N) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N))$
74	33	adantr	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω$
75		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
76	75	fveq2i	$⊢ rec (F, ⟨N, y⟩) (1_{𝑜}) = rec (F, ⟨N, y⟩) (suc \emptyset)$
77		rdgsuc	$⊢ \emptyset \in On \to rec (F, ⟨N, y⟩) (suc \emptyset) = F (rec (F, ⟨N, y⟩) (\emptyset))$
78	25 77	ax-mp	$⊢ rec (F, ⟨N, y⟩) (suc \emptyset) = F (rec (F, ⟨N, y⟩) (\emptyset))$
79		opex	$⊢ ⟨N, y⟩ \in V$
80	79	rdg0	$⊢ rec (F, ⟨N, y⟩) (\emptyset) = ⟨N, y⟩$
81	80	fveq2i	$⊢ F (rec (F, ⟨N, y⟩) (\emptyset)) = F (⟨N, y⟩)$
82	76 78 81	3eqtri	$⊢ rec (F, ⟨N, y⟩) (1_{𝑜}) = F (⟨N, y⟩)$
83	1	finxpreclem3	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to ⟨⋃ N, 1^{st} (y)⟩ = F (⟨N, y⟩)$
84	82 83	eqtr4id	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨N, y⟩) (1_{𝑜}) = ⟨⋃ N, 1^{st} (y)⟩$
85	84	fveq2d	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to F (rec (F, ⟨N, y⟩) (1_{𝑜})) = F (⟨⋃ N, 1^{st} (y)⟩)$
86		2on0	$⊢ 2_{𝑜} \neq \emptyset$
87		nnlim	$⊢ 2_{𝑜} \in ω \to \neg Lim 2_{𝑜}$
88	2 87	ax-mp	$⊢ \neg Lim 2_{𝑜}$
89		rdgsucuni	$⊢ (2_{𝑜} \in On \land 2_{𝑜} \neq \emptyset \land \neg Lim 2_{𝑜}) \to rec (F, ⟨N, y⟩) (2_{𝑜}) = F (rec (F, ⟨N, y⟩) (⋃ 2_{𝑜}))$
90	4 86 88 89	mp3an	$⊢ rec (F, ⟨N, y⟩) (2_{𝑜}) = F (rec (F, ⟨N, y⟩) (⋃ 2_{𝑜}))$
91		1oequni2o	$⊢ 1_{𝑜} = ⋃ 2_{𝑜}$
92	91	fveq2i	$⊢ rec (F, ⟨N, y⟩) (1_{𝑜}) = rec (F, ⟨N, y⟩) (⋃ 2_{𝑜})$
93	92	fveq2i	$⊢ F (rec (F, ⟨N, y⟩) (1_{𝑜})) = F (rec (F, ⟨N, y⟩) (⋃ 2_{𝑜}))$
94	90 93	eqtr4i	$⊢ rec (F, ⟨N, y⟩) (2_{𝑜}) = F (rec (F, ⟨N, y⟩) (1_{𝑜}))$
95	75	fveq2i	$⊢ rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜}) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (suc \emptyset)$
96		rdgsuc	$⊢ \emptyset \in On \to rec (F, ⟨⋃ N, 1^{st} (y)⟩) (suc \emptyset) = F (rec (F, ⟨⋃ N, 1^{st} (y)⟩) (\emptyset))$
97	25 96	ax-mp	$⊢ rec (F, ⟨⋃ N, 1^{st} (y)⟩) (suc \emptyset) = F (rec (F, ⟨⋃ N, 1^{st} (y)⟩) (\emptyset))$
98		opex	$⊢ ⟨⋃ N, 1^{st} (y)⟩ \in V$
99	98	rdg0	$⊢ rec (F, ⟨⋃ N, 1^{st} (y)⟩) (\emptyset) = ⟨⋃ N, 1^{st} (y)⟩$
100	99	fveq2i	$⊢ F (rec (F, ⟨⋃ N, 1^{st} (y)⟩) (\emptyset)) = F (⟨⋃ N, 1^{st} (y)⟩)$
101	95 97 100	3eqtri	$⊢ rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜}) = F (⟨⋃ N, 1^{st} (y)⟩)$
102	85 94 101	3eqtr4g	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨N, y⟩) (2_{𝑜}) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜})$
103		1on	$⊢ 1_{𝑜} \in On$
104		rdgeqoa	$⊢ (2_{𝑜} \in On \land 1_{𝑜} \in On \land (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω) \to (rec (F, ⟨N, y⟩) (2_{𝑜}) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜}) \to rec (F, ⟨N, y⟩) (2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)))$
105	4 103 104	mp3an12	$⊢ (ι o \in On \| 2_{𝑜} +_{𝑜} o = N) \in ω \to (rec (F, ⟨N, y⟩) (2_{𝑜}) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜}) \to rec (F, ⟨N, y⟩) (2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)))$
106	74 102 105	sylc	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨N, y⟩) (2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (1_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N))$
107	20	fveq2d	$⊢ (N \in ω \land 2_{𝑜} \subseteq N) \to rec (F, ⟨N, y⟩) (2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)) = rec (F, ⟨N, y⟩) (N)$
108	107	adantr	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨N, y⟩) (2_{𝑜} +_{𝑜} (ι o \in On \| 2_{𝑜} +_{𝑜} o = N)) = rec (F, ⟨N, y⟩) (N)$
109	73 106 108	3eqtr2rd	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨N, y⟩) (N) = rec (F, ⟨⋃ N, 1^{st} (y)⟩) (⋃ N)$

Metamath Proof Explorer

Theorem finxpreclem4

Proof