rdgeqoa

Description: If a recursive function with an initial value A at step N is equal to itself with an initial value B at step M , then every finite number of successor steps will also be equal. (Contributed by ML, 21-Oct-2020)

		Ref	Expression
	Assertion	rdgeqoa	$⊢ (N \in On \land M \in On \land X \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} X) = rec (F, B) (M +_{𝑜} X))$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (N \in On \land M \in On \land X \in ω) \to X \in ω$
2		eleq1	$⊢ x = X \to (x \in ω \leftrightarrow X \in ω)$
3	2	3anbi3d	$⊢ x = X \to ((N \in On \land M \in On \land x \in ω) \leftrightarrow (N \in On \land M \in On \land X \in ω))$
4		oveq2	$⊢ x = X \to N +_{𝑜} x = N +_{𝑜} X$
5	4	fveq2d	$⊢ x = X \to rec (F, A) (N +_{𝑜} x) = rec (F, A) (N +_{𝑜} X)$
6		oveq2	$⊢ x = X \to M +_{𝑜} x = M +_{𝑜} X$
7	6	fveq2d	$⊢ x = X \to rec (F, B) (M +_{𝑜} x) = rec (F, B) (M +_{𝑜} X)$
8	5 7	eqeq12d	$⊢ x = X \to (rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \leftrightarrow rec (F, A) (N +_{𝑜} X) = rec (F, B) (M +_{𝑜} X))$
9	8	imbi2d	$⊢ x = X \to ((rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \leftrightarrow (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} X) = rec (F, B) (M +_{𝑜} X)))$
10	3 9	imbi12d	$⊢ x = X \to (((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \leftrightarrow ((N \in On \land M \in On \land X \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} X) = rec (F, B) (M +_{𝑜} X))))$
11		peano1	$⊢ \emptyset \in ω$
12		oa0	$⊢ N \in On \to N +_{𝑜} \emptyset = N$
13	12	fveq2d	$⊢ N \in On \to rec (F, A) (N +_{𝑜} \emptyset) = rec (F, A) (N)$
14	13	eqcomd	$⊢ N \in On \to rec (F, A) (N) = rec (F, A) (N +_{𝑜} \emptyset)$
15		oa0	$⊢ M \in On \to M +_{𝑜} \emptyset = M$
16	15	fveq2d	$⊢ M \in On \to rec (F, B) (M +_{𝑜} \emptyset) = rec (F, B) (M)$
17	16	eqcomd	$⊢ M \in On \to rec (F, B) (M) = rec (F, B) (M +_{𝑜} \emptyset)$
18	14 17	eqeqan12d	$⊢ (N \in On \land M \in On) \to (rec (F, A) (N) = rec (F, B) (M) \leftrightarrow rec (F, A) (N +_{𝑜} \emptyset) = rec (F, B) (M +_{𝑜} \emptyset))$
19	18	biimpd	$⊢ (N \in On \land M \in On) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} \emptyset) = rec (F, B) (M +_{𝑜} \emptyset))$
20		eleq1	$⊢ x = \emptyset \to (x \in ω \leftrightarrow \emptyset \in ω)$
21	20	3anbi3d	$⊢ x = \emptyset \to ((N \in On \land M \in On \land x \in ω) \leftrightarrow (N \in On \land M \in On \land \emptyset \in ω))$
22	11	biantru	$⊢ M \in On \leftrightarrow (M \in On \land \emptyset \in ω)$
23	22	anbi2i	$⊢ (N \in On \land M \in On) \leftrightarrow (N \in On \land (M \in On \land \emptyset \in ω))$
24		3anass	$⊢ (N \in On \land M \in On \land \emptyset \in ω) \leftrightarrow (N \in On \land (M \in On \land \emptyset \in ω))$
25	23 24	bitr4i	$⊢ (N \in On \land M \in On) \leftrightarrow (N \in On \land M \in On \land \emptyset \in ω)$
26	21 25	bitr4di	$⊢ x = \emptyset \to ((N \in On \land M \in On \land x \in ω) \leftrightarrow (N \in On \land M \in On))$
27		oveq2	$⊢ x = \emptyset \to N +_{𝑜} x = N +_{𝑜} \emptyset$
28	27	fveq2d	$⊢ x = \emptyset \to rec (F, A) (N +_{𝑜} x) = rec (F, A) (N +_{𝑜} \emptyset)$
29		oveq2	$⊢ x = \emptyset \to M +_{𝑜} x = M +_{𝑜} \emptyset$
30	29	fveq2d	$⊢ x = \emptyset \to rec (F, B) (M +_{𝑜} x) = rec (F, B) (M +_{𝑜} \emptyset)$
31	28 30	eqeq12d	$⊢ x = \emptyset \to (rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \leftrightarrow rec (F, A) (N +_{𝑜} \emptyset) = rec (F, B) (M +_{𝑜} \emptyset))$
32	31	imbi2d	$⊢ x = \emptyset \to ((rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \leftrightarrow (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} \emptyset) = rec (F, B) (M +_{𝑜} \emptyset)))$
33	26 32	imbi12d	$⊢ x = \emptyset \to (((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \leftrightarrow ((N \in On \land M \in On) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} \emptyset) = rec (F, B) (M +_{𝑜} \emptyset))))$
34	19 33	mpbiri	$⊢ x = \emptyset \to ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)))$
35	34	ax-gen	$⊢ \forall x (x = \emptyset \to ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))))$
36		sbc6g	$⊢ \emptyset \in ω \to (\underset{˙}{[} \emptyset / x \underset{˙}{]} ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \leftrightarrow \forall x (x = \emptyset \to ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)))))$
37	35 36	mpbiri	$⊢ \emptyset \in ω \to \underset{˙}{[} \emptyset / x \underset{˙}{]} ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)))$
38	11 37	ax-mp	$⊢ \underset{˙}{[} \emptyset / x \underset{˙}{]} ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)))$
39		peano2b	$⊢ x \in ω \leftrightarrow suc x \in ω$
40	39	3anbi3i	$⊢ (N \in On \land M \in On \land x \in ω) \leftrightarrow (N \in On \land M \in On \land suc x \in ω)$
41	40	imbi1i	$⊢ ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \leftrightarrow ((N \in On \land M \in On \land suc x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)))$
42		nnon	$⊢ x \in ω \to x \in On$
43		oacl	$⊢ (N \in On \land x \in On) \to N +_{𝑜} x \in On$
44		oacl	$⊢ (M \in On \land x \in On) \to M +_{𝑜} x \in On$
45	43 44	anim12i	$⊢ ((N \in On \land x \in On) \land (M \in On \land x \in On)) \to (N +_{𝑜} x \in On \land M +_{𝑜} x \in On)$
46	45	3impdir	$⊢ (N \in On \land M \in On \land x \in On) \to (N +_{𝑜} x \in On \land M +_{𝑜} x \in On)$
47		rdgsuc	$⊢ N +_{𝑜} x \in On \to rec (F, A) (suc (N +_{𝑜} x)) = F (rec (F, A) (N +_{𝑜} x))$
48		fveq2	$⊢ rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \to F (rec (F, A) (N +_{𝑜} x)) = F (rec (F, B) (M +_{𝑜} x))$
49	47 48	sylan9eqr	$⊢ (rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \land N +_{𝑜} x \in On) \to rec (F, A) (suc (N +_{𝑜} x)) = F (rec (F, B) (M +_{𝑜} x))$
50	49	adantrr	$⊢ (rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \land (N +_{𝑜} x \in On \land M +_{𝑜} x \in On)) \to rec (F, A) (suc (N +_{𝑜} x)) = F (rec (F, B) (M +_{𝑜} x))$
51		rdgsuc	$⊢ M +_{𝑜} x \in On \to rec (F, B) (suc (M +_{𝑜} x)) = F (rec (F, B) (M +_{𝑜} x))$
52	51	ad2antll	$⊢ (rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \land (N +_{𝑜} x \in On \land M +_{𝑜} x \in On)) \to rec (F, B) (suc (M +_{𝑜} x)) = F (rec (F, B) (M +_{𝑜} x))$
53	50 52	eqtr4d	$⊢ (rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \land (N +_{𝑜} x \in On \land M +_{𝑜} x \in On)) \to rec (F, A) (suc (N +_{𝑜} x)) = rec (F, B) (suc (M +_{𝑜} x))$
54	46 53	sylan2	$⊢ (rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \land (N \in On \land M \in On \land x \in On)) \to rec (F, A) (suc (N +_{𝑜} x)) = rec (F, B) (suc (M +_{𝑜} x))$
55	54	ancoms	$⊢ ((N \in On \land M \in On \land x \in On) \land rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \to rec (F, A) (suc (N +_{𝑜} x)) = rec (F, B) (suc (M +_{𝑜} x))$
56	42 55	syl3anl3	$⊢ ((N \in On \land M \in On \land x \in ω) \land rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \to rec (F, A) (suc (N +_{𝑜} x)) = rec (F, B) (suc (M +_{𝑜} x))$
57		onasuc	$⊢ (N \in On \land x \in ω) \to N +_{𝑜} suc x = suc (N +_{𝑜} x)$
58	57	fveq2d	$⊢ (N \in On \land x \in ω) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, A) (suc (N +_{𝑜} x))$
59	58	3adant2	$⊢ (N \in On \land M \in On \land x \in ω) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, A) (suc (N +_{𝑜} x))$
60	59	adantr	$⊢ ((N \in On \land M \in On \land x \in ω) \land rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, A) (suc (N +_{𝑜} x))$
61		onasuc	$⊢ (M \in On \land x \in ω) \to M +_{𝑜} suc x = suc (M +_{𝑜} x)$
62	61	fveq2d	$⊢ (M \in On \land x \in ω) \to rec (F, B) (M +_{𝑜} suc x) = rec (F, B) (suc (M +_{𝑜} x))$
63	62	3adant1	$⊢ (N \in On \land M \in On \land x \in ω) \to rec (F, B) (M +_{𝑜} suc x) = rec (F, B) (suc (M +_{𝑜} x))$
64	63	adantr	$⊢ ((N \in On \land M \in On \land x \in ω) \land rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \to rec (F, B) (M +_{𝑜} suc x) = rec (F, B) (suc (M +_{𝑜} x))$
65	56 60 64	3eqtr4d	$⊢ ((N \in On \land M \in On \land x \in ω) \land rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x)$
66	65	ex	$⊢ (N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x))$
67	66	imim2d	$⊢ (N \in On \land M \in On \land x \in ω) \to ((rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x)))$
68	40 67	sylbir	$⊢ (N \in On \land M \in On \land suc x \in ω) \to ((rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x)))$
69	68	a2i	$⊢ ((N \in On \land M \in On \land suc x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \to ((N \in On \land M \in On \land suc x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x)))$
70	41 69	sylbi	$⊢ ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \to ((N \in On \land M \in On \land suc x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x)))$
71		sbcimg	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \leftrightarrow (\underset{˙}{[} suc x / x \underset{˙}{]} (N \in On \land M \in On \land x \in ω) \to \underset{˙}{[} suc x / x \underset{˙}{]} (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))))$
72		sbc3an	$⊢ \underset{˙}{[} suc x / x \underset{˙}{]} (N \in On \land M \in On \land x \in ω) \leftrightarrow (\underset{˙}{[} suc x / x \underset{˙}{]} N \in On \land \underset{˙}{[} suc x / x \underset{˙}{]} M \in On \land \underset{˙}{[} suc x / x \underset{˙}{]} x \in ω)$
73		sbcg	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} N \in On \leftrightarrow N \in On)$
74		sbcg	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} M \in On \leftrightarrow M \in On)$
75		sbcel1v	$⊢ \underset{˙}{[} suc x / x \underset{˙}{]} x \in ω \leftrightarrow suc x \in ω$
76	75	a1i	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} x \in ω \leftrightarrow suc x \in ω)$
77	73 74 76	3anbi123d	$⊢ suc x \in ω \to ((\underset{˙}{[} suc x / x \underset{˙}{]} N \in On \land \underset{˙}{[} suc x / x \underset{˙}{]} M \in On \land \underset{˙}{[} suc x / x \underset{˙}{]} x \in ω) \leftrightarrow (N \in On \land M \in On \land suc x \in ω))$
78	72 77	syl5bb	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} (N \in On \land M \in On \land x \in ω) \leftrightarrow (N \in On \land M \in On \land suc x \in ω))$
79		sbcimg	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \leftrightarrow (\underset{˙}{[} suc x / x \underset{˙}{]} rec (F, A) (N) = rec (F, B) (M) \to \underset{˙}{[} suc x / x \underset{˙}{]} rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)))$
80		sbcg	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} rec (F, A) (N) = rec (F, B) (M) \leftrightarrow rec (F, A) (N) = rec (F, B) (M))$
81		sbceqg	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \leftrightarrow ⦋ suc x / x ⦌ rec (F, A) (N +_{𝑜} x) = ⦋ suc x / x ⦌ rec (F, B) (M +_{𝑜} x))$
82		csbfv12	$⊢ ⦋ suc x / x ⦌ rec (F, A) (N +_{𝑜} x) = ⦋ suc x / x ⦌ rec (F, A) (⦋ suc x / x ⦌ (N +_{𝑜} x))$
83		csbconstg	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ rec (F, A) = rec (F, A)$
84		csbov123	$⊢ ⦋ suc x / x ⦌ (N +_{𝑜} x) = ⦋ suc x / x ⦌ N ⦋ suc x / x ⦌ +_{𝑜} ⦋ suc x / x ⦌ x$
85		csbconstg	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ +_{𝑜} = +_{𝑜}$
86		csbconstg	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ N = N$
87		csbvarg	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ x = suc x$
88	85 86 87	oveq123d	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ N ⦋ suc x / x ⦌ +_{𝑜} ⦋ suc x / x ⦌ x = N +_{𝑜} suc x$
89	84 88	syl5eq	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ (N +_{𝑜} x) = N +_{𝑜} suc x$
90	83 89	fveq12d	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ rec (F, A) (⦋ suc x / x ⦌ (N +_{𝑜} x)) = rec (F, A) (N +_{𝑜} suc x)$
91	82 90	syl5eq	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ rec (F, A) (N +_{𝑜} x) = rec (F, A) (N +_{𝑜} suc x)$
92		csbfv12	$⊢ ⦋ suc x / x ⦌ rec (F, B) (M +_{𝑜} x) = ⦋ suc x / x ⦌ rec (F, B) (⦋ suc x / x ⦌ (M +_{𝑜} x))$
93		csbconstg	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ rec (F, B) = rec (F, B)$
94		csbov123	$⊢ ⦋ suc x / x ⦌ (M +_{𝑜} x) = ⦋ suc x / x ⦌ M ⦋ suc x / x ⦌ +_{𝑜} ⦋ suc x / x ⦌ x$
95		csbconstg	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ M = M$
96	85 95 87	oveq123d	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ M ⦋ suc x / x ⦌ +_{𝑜} ⦋ suc x / x ⦌ x = M +_{𝑜} suc x$
97	94 96	syl5eq	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ (M +_{𝑜} x) = M +_{𝑜} suc x$
98	93 97	fveq12d	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ rec (F, B) (⦋ suc x / x ⦌ (M +_{𝑜} x)) = rec (F, B) (M +_{𝑜} suc x)$
99	92 98	syl5eq	$⊢ suc x \in ω \to ⦋ suc x / x ⦌ rec (F, B) (M +_{𝑜} x) = rec (F, B) (M +_{𝑜} suc x)$
100	91 99	eqeq12d	$⊢ suc x \in ω \to (⦋ suc x / x ⦌ rec (F, A) (N +_{𝑜} x) = ⦋ suc x / x ⦌ rec (F, B) (M +_{𝑜} x) \leftrightarrow rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x))$
101	81 100	bitrd	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x) \leftrightarrow rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x))$
102	80 101	imbi12d	$⊢ suc x \in ω \to ((\underset{˙}{[} suc x / x \underset{˙}{]} rec (F, A) (N) = rec (F, B) (M) \to \underset{˙}{[} suc x / x \underset{˙}{]} rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \leftrightarrow (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x)))$
103	79 102	bitrd	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)) \leftrightarrow (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x)))$
104	78 103	imbi12d	$⊢ suc x \in ω \to ((\underset{˙}{[} suc x / x \underset{˙}{]} (N \in On \land M \in On \land x \in ω) \to \underset{˙}{[} suc x / x \underset{˙}{]} (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \leftrightarrow ((N \in On \land M \in On \land suc x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x))))$
105	71 104	bitrd	$⊢ suc x \in ω \to (\underset{˙}{[} suc x / x \underset{˙}{]} ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \leftrightarrow ((N \in On \land M \in On \land suc x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} suc x) = rec (F, B) (M +_{𝑜} suc x))))$
106	70 105	syl5ibr	$⊢ suc x \in ω \to (((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \to \underset{˙}{[} suc x / x \underset{˙}{]} ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))))$
107	39 106	sylbi	$⊢ x \in ω \to (((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))) \to \underset{˙}{[} suc x / x \underset{˙}{]} ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x))))$
108	38 107	findes	$⊢ x \in ω \to ((N \in On \land M \in On \land x \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} x) = rec (F, B) (M +_{𝑜} x)))$
109	10 108	vtoclga	$⊢ X \in ω \to ((N \in On \land M \in On \land X \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} X) = rec (F, B) (M +_{𝑜} X)))$
110	1 109	mpcom	$⊢ (N \in On \land M \in On \land X \in ω) \to (rec (F, A) (N) = rec (F, B) (M) \to rec (F, A) (N +_{𝑜} X) = rec (F, B) (M +_{𝑜} X))$

Metamath Proof Explorer

Theorem rdgeqoa

Proof