fineqvnttrclselem3

	Ref	Expression
Hypotheses	fineqvnttrclselem3.1	$⊢ R = \{⟨x, y⟩ \| (x \in A \land x = suc y)\}$
	fineqvnttrclselem3.2	$⊢ A = ω$
	fineqvnttrclselem3.3	$⊢ F = (v \in suc suc N ⟼ ⋃ \{d \in On \| v +_{𝑜} d = B\})$
Assertion	fineqvnttrclselem3	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B) \to \forall a \in suc N F (a) R F (suc a)$

Proof

Step	Hyp	Ref	Expression
1		fineqvnttrclselem3.1	$⊢ R = \{⟨x, y⟩ \| (x \in A \land x = suc y)\}$
2		fineqvnttrclselem3.2	$⊢ A = ω$
3		fineqvnttrclselem3.3	$⊢ F = (v \in suc suc N ⟼ ⋃ \{d \in On \| v +_{𝑜} d = B\})$
4		oveq1	$⊢ v = a \to v +_{𝑜} d = a +_{𝑜} d$
5	4	eqeq1d	$⊢ v = a \to (v +_{𝑜} d = B \leftrightarrow a +_{𝑜} d = B)$
6	5	rabbidv	$⊢ v = a \to \{d \in On \| v +_{𝑜} d = B\} = \{d \in On \| a +_{𝑜} d = B\}$
7	6	unieqd	$⊢ v = a \to ⋃ \{d \in On \| v +_{𝑜} d = B\} = ⋃ \{d \in On \| a +_{𝑜} d = B\}$
8		elelsuc	$⊢ a \in suc N \to a \in suc suc N$
9	8	adantl	$⊢ (B \in (ω ∖ 1_{𝑜}) \land a \in suc N) \to a \in suc suc N$
10		fineqvnttrclselem1	$⊢ B \in (ω ∖ 1_{𝑜}) \to ⋃ \{d \in On \| a +_{𝑜} d = B\} \in ω$
11	10	adantr	$⊢ (B \in (ω ∖ 1_{𝑜}) \land a \in suc N) \to ⋃ \{d \in On \| a +_{𝑜} d = B\} \in ω$
12	3 7 9 11	fvmptd3	$⊢ (B \in (ω ∖ 1_{𝑜}) \land a \in suc N) \to F (a) = ⋃ \{d \in On \| a +_{𝑜} d = B\}$
13	12 11	eqeltrd	$⊢ (B \in (ω ∖ 1_{𝑜}) \land a \in suc N) \to F (a) \in ω$
14	13	3adant2	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to F (a) \in ω$
15	14 2	eleqtrrdi	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to F (a) \in A$
16	3	fineqvnttrclselem2	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc suc N) \to a +_{𝑜} F (a) = B$
17	8 16	syl3an3	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to a +_{𝑜} F (a) = B$
18		eldifi	$⊢ B \in (ω ∖ 1_{𝑜}) \to B \in ω$
19		elnn	$⊢ (N \in B \land B \in ω) \to N \in ω$
20	19	ancoms	$⊢ (B \in ω \land N \in B) \to N \in ω$
21	18 20	sylan	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B) \to N \in ω$
22		peano2	$⊢ N \in ω \to suc N \in ω$
23		nnord	$⊢ suc N \in ω \to Ord suc N$
24		ordsucelsuc	$⊢ Ord suc N \to (a \in suc N \leftrightarrow suc a \in suc suc N)$
25	22 23 24	3syl	$⊢ N \in ω \to (a \in suc N \leftrightarrow suc a \in suc suc N)$
26	25	biimpa	$⊢ (N \in ω \land a \in suc N) \to suc a \in suc suc N$
27	21 26	stoic3	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to suc a \in suc suc N$
28	3	fineqvnttrclselem2	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land suc a \in suc suc N) \to suc a +_{𝑜} F (suc a) = B$
29	27 28	syld3an3	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to suc a +_{𝑜} F (suc a) = B$
30	17 29	eqtr4d	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to a +_{𝑜} F (a) = suc a +_{𝑜} F (suc a)$
31	21 22	syl	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B) \to suc N \in ω$
32		elnn	$⊢ (a \in suc N \land suc N \in ω) \to a \in ω$
33	32	ancoms	$⊢ (suc N \in ω \land a \in suc N) \to a \in ω$
34	31 33	stoic3	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to a \in ω$
35	21	3adant3	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to N \in ω$
36		oveq1	$⊢ v = suc a \to v +_{𝑜} d = suc a +_{𝑜} d$
37	36	eqeq1d	$⊢ v = suc a \to (v +_{𝑜} d = B \leftrightarrow suc a +_{𝑜} d = B)$
38	37	rabbidv	$⊢ v = suc a \to \{d \in On \| v +_{𝑜} d = B\} = \{d \in On \| suc a +_{𝑜} d = B\}$
39	38	unieqd	$⊢ v = suc a \to ⋃ \{d \in On \| v +_{𝑜} d = B\} = ⋃ \{d \in On \| suc a +_{𝑜} d = B\}$
40	26	3adant1	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in ω \land a \in suc N) \to suc a \in suc suc N$
41		fineqvnttrclselem1	$⊢ B \in (ω ∖ 1_{𝑜}) \to ⋃ \{d \in On \| suc a +_{𝑜} d = B\} \in ω$
42	41	3ad2ant1	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in ω \land a \in suc N) \to ⋃ \{d \in On \| suc a +_{𝑜} d = B\} \in ω$
43	3 39 40 42	fvmptd3	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in ω \land a \in suc N) \to F (suc a) = ⋃ \{d \in On \| suc a +_{𝑜} d = B\}$
44	43 42	eqeltrd	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in ω \land a \in suc N) \to F (suc a) \in ω$
45	35 44	syld3an2	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to F (suc a) \in ω$
46		nnacom	$⊢ (a \in ω \land F (suc a) \in ω) \to a +_{𝑜} F (suc a) = F (suc a) +_{𝑜} a$
47	46	suceqd	$⊢ (a \in ω \land F (suc a) \in ω) \to suc (a +_{𝑜} F (suc a)) = suc (F (suc a) +_{𝑜} a)$
48		nnasuc	$⊢ (a \in ω \land F (suc a) \in ω) \to a +_{𝑜} suc F (suc a) = suc (a +_{𝑜} F (suc a))$
49		nnasuc	$⊢ (F (suc a) \in ω \land a \in ω) \to F (suc a) +_{𝑜} suc a = suc (F (suc a) +_{𝑜} a)$
50	49	ancoms	$⊢ (a \in ω \land F (suc a) \in ω) \to F (suc a) +_{𝑜} suc a = suc (F (suc a) +_{𝑜} a)$
51	47 48 50	3eqtr4d	$⊢ (a \in ω \land F (suc a) \in ω) \to a +_{𝑜} suc F (suc a) = F (suc a) +_{𝑜} suc a$
52		peano2	$⊢ a \in ω \to suc a \in ω$
53		nnacom	$⊢ (suc a \in ω \land F (suc a) \in ω) \to suc a +_{𝑜} F (suc a) = F (suc a) +_{𝑜} suc a$
54	52 53	sylan	$⊢ (a \in ω \land F (suc a) \in ω) \to suc a +_{𝑜} F (suc a) = F (suc a) +_{𝑜} suc a$
55	51 54	eqtr4d	$⊢ (a \in ω \land F (suc a) \in ω) \to a +_{𝑜} suc F (suc a) = suc a +_{𝑜} F (suc a)$
56	55	3adant2	$⊢ (a \in ω \land F (a) \in ω \land F (suc a) \in ω) \to a +_{𝑜} suc F (suc a) = suc a +_{𝑜} F (suc a)$
57	56	eqeq2d	$⊢ (a \in ω \land F (a) \in ω \land F (suc a) \in ω) \to (a +_{𝑜} F (a) = a +_{𝑜} suc F (suc a) \leftrightarrow a +_{𝑜} F (a) = suc a +_{𝑜} F (suc a))$
58		peano2	$⊢ F (suc a) \in ω \to suc F (suc a) \in ω$
59		nnacan	$⊢ (a \in ω \land F (a) \in ω \land suc F (suc a) \in ω) \to (a +_{𝑜} F (a) = a +_{𝑜} suc F (suc a) \leftrightarrow F (a) = suc F (suc a))$
60	58 59	syl3an3	$⊢ (a \in ω \land F (a) \in ω \land F (suc a) \in ω) \to (a +_{𝑜} F (a) = a +_{𝑜} suc F (suc a) \leftrightarrow F (a) = suc F (suc a))$
61	57 60	bitr3d	$⊢ (a \in ω \land F (a) \in ω \land F (suc a) \in ω) \to (a +_{𝑜} F (a) = suc a +_{𝑜} F (suc a) \leftrightarrow F (a) = suc F (suc a))$
62	34 14 45 61	syl3anc	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to (a +_{𝑜} F (a) = suc a +_{𝑜} F (suc a) \leftrightarrow F (a) = suc F (suc a))$
63	30 62	mpbid	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to F (a) = suc F (suc a)$
64		fvex	$⊢ F (a) \in V$
65		fvex	$⊢ F (suc a) \in V$
66		eleq1	$⊢ x = F (a) \to (x \in A \leftrightarrow F (a) \in A)$
67		eqeq1	$⊢ x = F (a) \to (x = suc y \leftrightarrow F (a) = suc y)$
68	66 67	anbi12d	$⊢ x = F (a) \to ((x \in A \land x = suc y) \leftrightarrow (F (a) \in A \land F (a) = suc y))$
69		suceq	$⊢ y = F (suc a) \to suc y = suc F (suc a)$
70	69	eqeq2d	$⊢ y = F (suc a) \to (F (a) = suc y \leftrightarrow F (a) = suc F (suc a))$
71	70	anbi2d	$⊢ y = F (suc a) \to ((F (a) \in A \land F (a) = suc y) \leftrightarrow (F (a) \in A \land F (a) = suc F (suc a)))$
72	64 65 68 71 1	brab	$⊢ F (a) R F (suc a) \leftrightarrow (F (a) \in A \land F (a) = suc F (suc a))$
73	15 63 72	sylanbrc	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B \land a \in suc N) \to F (a) R F (suc a)$
74	73	3expia	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B) \to (a \in suc N \to F (a) R F (suc a))$
75	74	ralrimiv	$⊢ (B \in (ω ∖ 1_{𝑜}) \land N \in B) \to \forall a \in suc N F (a) R F (suc a)$

Metamath Proof Explorer

Theorem fineqvnttrclselem3

Proof