ttrclselem2

Description: Lemma for ttrclse . Show that a suc N element long chain gives membership in the N -th predecessor class and vice-versa. (Contributed by Scott Fenton, 31-Oct-2024)

		Ref	Expression
	Hypothesis	ttrclselem.1	$⊢ F = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X))$
	Assertion	ttrclselem2	$⊢ (N \in ω \land R Se A \land X \in A) \to (\exists f (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (N))$

Proof

Step	Hyp	Ref	Expression
1		ttrclselem.1	$⊢ F = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X))$
2		suceq	$⊢ m = \emptyset \to suc m = suc \emptyset$
3		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
4	2 3	eqtr4di	$⊢ m = \emptyset \to suc m = 1_{𝑜}$
5		suceq	$⊢ suc m = 1_{𝑜} \to suc suc m = suc 1_{𝑜}$
6	4 5	syl	$⊢ m = \emptyset \to suc suc m = suc 1_{𝑜}$
7	6	fneq2d	$⊢ m = \emptyset \to (f Fn suc suc m \leftrightarrow f Fn suc 1_{𝑜})$
8	4	fveqeq2d	$⊢ m = \emptyset \to (f (suc m) = X \leftrightarrow f (1_{𝑜}) = X)$
9	8	anbi2d	$⊢ m = \emptyset \to ((f (\emptyset) = y \land f (suc m) = X) \leftrightarrow (f (\emptyset) = y \land f (1_{𝑜}) = X))$
10		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
11	4 10	eqtrdi	$⊢ m = \emptyset \to suc m = \{\emptyset\}$
12	11	raleqdv	$⊢ m = \emptyset \to (\forall a \in suc m f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow \forall a \in \{\emptyset\} f (a) ({R ↾}_{A}) f (suc a))$
13		0ex	$⊢ \emptyset \in V$
14		fveq2	$⊢ a = \emptyset \to f (a) = f (\emptyset)$
15		suceq	$⊢ a = \emptyset \to suc a = suc \emptyset$
16	15 3	eqtr4di	$⊢ a = \emptyset \to suc a = 1_{𝑜}$
17	16	fveq2d	$⊢ a = \emptyset \to f (suc a) = f (1_{𝑜})$
18	14 17	breq12d	$⊢ a = \emptyset \to (f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow f (\emptyset) ({R ↾}_{A}) f (1_{𝑜}))$
19	13 18	ralsn	$⊢ \forall a \in \{\emptyset\} f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})$
20	12 19	bitrdi	$⊢ m = \emptyset \to (\forall a \in suc m f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow f (\emptyset) ({R ↾}_{A}) f (1_{𝑜}))$
21	7 9 20	3anbi123d	$⊢ m = \emptyset \to ((f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})))$
22	21	exbidv	$⊢ m = \emptyset \to (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})))$
23		fveq2	$⊢ m = \emptyset \to F (m) = F (\emptyset)$
24	23	eleq2d	$⊢ m = \emptyset \to (y \in F (m) \leftrightarrow y \in F (\emptyset))$
25	22 24	bibi12d	$⊢ m = \emptyset \to ((\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow y \in F (\emptyset)))$
26	25	albidv	$⊢ m = \emptyset \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow \forall y (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow y \in F (\emptyset)))$
27	26	imbi2d	$⊢ m = \emptyset \to (((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m))) \leftrightarrow ((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow y \in F (\emptyset))))$
28		suceq	$⊢ m = n \to suc m = suc n$
29		suceq	$⊢ suc m = suc n \to suc suc m = suc suc n$
30	28 29	syl	$⊢ m = n \to suc suc m = suc suc n$
31	30	fneq2d	$⊢ m = n \to (f Fn suc suc m \leftrightarrow f Fn suc suc n)$
32	28	fveqeq2d	$⊢ m = n \to (f (suc m) = X \leftrightarrow f (suc n) = X)$
33	32	anbi2d	$⊢ m = n \to ((f (\emptyset) = y \land f (suc m) = X) \leftrightarrow (f (\emptyset) = y \land f (suc n) = X))$
34	28	raleqdv	$⊢ m = n \to (\forall a \in suc m f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow \forall a \in suc n f (a) ({R ↾}_{A}) f (suc a))$
35		fveq2	$⊢ a = c \to f (a) = f (c)$
36		suceq	$⊢ a = c \to suc a = suc c$
37	36	fveq2d	$⊢ a = c \to f (suc a) = f (suc c)$
38	35 37	breq12d	$⊢ a = c \to (f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow f (c) ({R ↾}_{A}) f (suc c))$
39	38	cbvralvw	$⊢ \forall a \in suc n f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow \forall c \in suc n f (c) ({R ↾}_{A}) f (suc c)$
40	34 39	bitrdi	$⊢ m = n \to (\forall a \in suc m f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow \forall c \in suc n f (c) ({R ↾}_{A}) f (suc c))$
41	31 33 40	3anbi123d	$⊢ m = n \to ((f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow (f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = X) \land \forall c \in suc n f (c) ({R ↾}_{A}) f (suc c)))$
42	41	exbidv	$⊢ m = n \to (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists f (f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = X) \land \forall c \in suc n f (c) ({R ↾}_{A}) f (suc c)))$
43		fneq1	$⊢ f = g \to (f Fn suc suc n \leftrightarrow g Fn suc suc n)$
44		fveq1	$⊢ f = g \to f (\emptyset) = g (\emptyset)$
45	44	eqeq1d	$⊢ f = g \to (f (\emptyset) = y \leftrightarrow g (\emptyset) = y)$
46		fveq1	$⊢ f = g \to f (suc n) = g (suc n)$
47	46	eqeq1d	$⊢ f = g \to (f (suc n) = X \leftrightarrow g (suc n) = X)$
48	45 47	anbi12d	$⊢ f = g \to ((f (\emptyset) = y \land f (suc n) = X) \leftrightarrow (g (\emptyset) = y \land g (suc n) = X))$
49		fveq1	$⊢ f = g \to f (c) = g (c)$
50		fveq1	$⊢ f = g \to f (suc c) = g (suc c)$
51	49 50	breq12d	$⊢ f = g \to (f (c) ({R ↾}_{A}) f (suc c) \leftrightarrow g (c) ({R ↾}_{A}) g (suc c))$
52	51	ralbidv	$⊢ f = g \to (\forall c \in suc n f (c) ({R ↾}_{A}) f (suc c) \leftrightarrow \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c))$
53	43 48 52	3anbi123d	$⊢ f = g \to ((f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = X) \land \forall c \in suc n f (c) ({R ↾}_{A}) f (suc c)) \leftrightarrow (g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)))$
54	53	cbvexvw	$⊢ \exists f (f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = X) \land \forall c \in suc n f (c) ({R ↾}_{A}) f (suc c)) \leftrightarrow \exists g (g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c))$
55	42 54	bitrdi	$⊢ m = n \to (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists g (g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)))$
56		fveq2	$⊢ m = n \to F (m) = F (n)$
57	56	eleq2d	$⊢ m = n \to (y \in F (m) \leftrightarrow y \in F (n))$
58	55 57	bibi12d	$⊢ m = n \to ((\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow (\exists g (g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow y \in F (n)))$
59	58	albidv	$⊢ m = n \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow \forall y (\exists g (g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow y \in F (n)))$
60		eqeq2	$⊢ y = z \to (g (\emptyset) = y \leftrightarrow g (\emptyset) = z)$
61	60	anbi1d	$⊢ y = z \to ((g (\emptyset) = y \land g (suc n) = X) \leftrightarrow (g (\emptyset) = z \land g (suc n) = X))$
62	61	3anbi2d	$⊢ y = z \to ((g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)))$
63	62	exbidv	$⊢ y = z \to (\exists g (g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow \exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)))$
64		eleq1	$⊢ y = z \to (y \in F (n) \leftrightarrow z \in F (n))$
65	63 64	bibi12d	$⊢ y = z \to ((\exists g (g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow y \in F (n)) \leftrightarrow (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n)))$
66	65	cbvalvw	$⊢ \forall y (\exists g (g Fn suc suc n \land (g (\emptyset) = y \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow y \in F (n)) \leftrightarrow \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))$
67	59 66	bitrdi	$⊢ m = n \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n)))$
68	67	imbi2d	$⊢ m = n \to (((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m))) \leftrightarrow ((R Se A \land X \in A) \to \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))))$
69		suceq	$⊢ m = suc n \to suc m = suc suc n$
70		suceq	$⊢ suc m = suc suc n \to suc suc m = suc suc suc n$
71	69 70	syl	$⊢ m = suc n \to suc suc m = suc suc suc n$
72	71	fneq2d	$⊢ m = suc n \to (f Fn suc suc m \leftrightarrow f Fn suc suc suc n)$
73	69	fveqeq2d	$⊢ m = suc n \to (f (suc m) = X \leftrightarrow f (suc suc n) = X)$
74	73	anbi2d	$⊢ m = suc n \to ((f (\emptyset) = y \land f (suc m) = X) \leftrightarrow (f (\emptyset) = y \land f (suc suc n) = X))$
75	69	raleqdv	$⊢ m = suc n \to (\forall a \in suc m f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))$
76	72 74 75	3anbi123d	$⊢ m = suc n \to ((f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)))$
77	76	exbidv	$⊢ m = suc n \to (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)))$
78		fveq2	$⊢ m = suc n \to F (m) = F (suc n)$
79	78	eleq2d	$⊢ m = suc n \to (y \in F (m) \leftrightarrow y \in F (suc n))$
80	77 79	bibi12d	$⊢ m = suc n \to ((\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (suc n)))$
81	80	albidv	$⊢ m = suc n \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow \forall y (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (suc n)))$
82	81	imbi2d	$⊢ m = suc n \to (((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m))) \leftrightarrow ((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (suc n))))$
83		suceq	$⊢ m = N \to suc m = suc N$
84		suceq	$⊢ suc m = suc N \to suc suc m = suc suc N$
85	83 84	syl	$⊢ m = N \to suc suc m = suc suc N$
86	85	fneq2d	$⊢ m = N \to (f Fn suc suc m \leftrightarrow f Fn suc suc N)$
87	83	fveqeq2d	$⊢ m = N \to (f (suc m) = X \leftrightarrow f (suc N) = X)$
88	87	anbi2d	$⊢ m = N \to ((f (\emptyset) = y \land f (suc m) = X) \leftrightarrow (f (\emptyset) = y \land f (suc N) = X))$
89	83	raleqdv	$⊢ m = N \to (\forall a \in suc m f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a))$
90	86 88 89	3anbi123d	$⊢ m = N \to ((f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)))$
91	90	exbidv	$⊢ m = N \to (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists f (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)))$
92		fveq2	$⊢ m = N \to F (m) = F (N)$
93	92	eleq2d	$⊢ m = N \to (y \in F (m) \leftrightarrow y \in F (N))$
94	91 93	bibi12d	$⊢ m = N \to ((\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow (\exists f (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (N)))$
95	94	albidv	$⊢ m = N \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m)) \leftrightarrow \forall y (\exists f (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (N)))$
96	95	imbi2d	$⊢ m = N \to (((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = y \land f (suc m) = X) \land \forall a \in suc m f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (m))) \leftrightarrow ((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (N))))$
97		eqeq2	$⊢ x = X \to (f (1_{𝑜}) = x \leftrightarrow f (1_{𝑜}) = X)$
98	97	anbi2d	$⊢ x = X \to ((f (\emptyset) = y \land f (1_{𝑜}) = x) \leftrightarrow (f (\emptyset) = y \land f (1_{𝑜}) = X))$
99	98	anbi2d	$⊢ x = X \to ((f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = x)) \leftrightarrow (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)))$
100	99	exbidv	$⊢ x = X \to (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = x)) \leftrightarrow \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)))$
101		vex	$⊢ y \in V$
102		vex	$⊢ x \in V$
103	101 102	ifex	$⊢ if (b = \emptyset, y, x) \in V$
104		eqid	$⊢ (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x))$
105	103 104	fnmpti	$⊢ (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) Fn suc 1_{𝑜}$
106		equid	$⊢ y = y$
107		equid	$⊢ x = x$
108	106 107	pm3.2i	$⊢ (y = y \land x = x)$
109		1oex	$⊢ 1_{𝑜} \in V$
110	109	sucex	$⊢ suc 1_{𝑜} \in V$
111	110	mptex	$⊢ (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \in V$
112		fneq1	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to (f Fn suc 1_{𝑜} \leftrightarrow (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) Fn suc 1_{𝑜})$
113		fveq1	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to f (\emptyset) = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) (\emptyset)$
114		1on	$⊢ 1_{𝑜} \in On$
115	114	onordi	$⊢ Ord 1_{𝑜}$
116		0elsuc	$⊢ Ord 1_{𝑜} \to \emptyset \in suc 1_{𝑜}$
117		iftrue	$⊢ b = \emptyset \to if (b = \emptyset, y, x) = y$
118	117 104 101	fvmpt	$⊢ \emptyset \in suc 1_{𝑜} \to (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) (\emptyset) = y$
119	115 116 118	mp2b	$⊢ (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) (\emptyset) = y$
120	113 119	eqtrdi	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to f (\emptyset) = y$
121	120	eqeq1d	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to (f (\emptyset) = y \leftrightarrow y = y)$
122		fveq1	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to f (1_{𝑜}) = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) (1_{𝑜})$
123	109	sucid	$⊢ 1_{𝑜} \in suc 1_{𝑜}$
124		eqeq1	$⊢ b = 1_{𝑜} \to (b = \emptyset \leftrightarrow 1_{𝑜} = \emptyset)$
125	124	ifbid	$⊢ b = 1_{𝑜} \to if (b = \emptyset, y, x) = if (1_{𝑜} = \emptyset, y, x)$
126		1n0	$⊢ 1_{𝑜} \neq \emptyset$
127	126	neii	$⊢ \neg 1_{𝑜} = \emptyset$
128	127	iffalsei	$⊢ if (1_{𝑜} = \emptyset, y, x) = x$
129	125 128	eqtrdi	$⊢ b = 1_{𝑜} \to if (b = \emptyset, y, x) = x$
130	129 104 102	fvmpt	$⊢ 1_{𝑜} \in suc 1_{𝑜} \to (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) (1_{𝑜}) = x$
131	123 130	ax-mp	$⊢ (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) (1_{𝑜}) = x$
132	122 131	eqtrdi	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to f (1_{𝑜}) = x$
133	132	eqeq1d	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to (f (1_{𝑜}) = x \leftrightarrow x = x)$
134	121 133	anbi12d	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to ((f (\emptyset) = y \land f (1_{𝑜}) = x) \leftrightarrow (y = y \land x = x))$
135	112 134	anbi12d	$⊢ f = (b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) \to ((f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = x)) \leftrightarrow ((b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) Fn suc 1_{𝑜} \land (y = y \land x = x)))$
136	111 135	spcev	$⊢ ((b \in suc 1_{𝑜} ⟼ if (b = \emptyset, y, x)) Fn suc 1_{𝑜} \land (y = y \land x = x)) \to \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = x))$
137	105 108 136	mp2an	$⊢ \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = x))$
138	100 137	vtoclg	$⊢ X \in A \to \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X))$
139	138	adantl	$⊢ (R Se A \land X \in A) \to \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X))$
140	139	biantrurd	$⊢ (R Se A \land X \in A) \to ((y \in A \land y R X) \leftrightarrow (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land (y \in A \land y R X)))$
141	101	elpred	$⊢ X \in A \to (y \in Pred (R, A, X) \leftrightarrow (y \in A \land y R X))$
142	141	adantl	$⊢ (R Se A \land X \in A) \to (y \in Pred (R, A, X) \leftrightarrow (y \in A \land y R X))$
143		brres	$⊢ X \in A \to (y ({R ↾}_{A}) X \leftrightarrow (y \in A \land y R X))$
144	143	adantl	$⊢ (R Se A \land X \in A) \to (y ({R ↾}_{A}) X \leftrightarrow (y \in A \land y R X))$
145	144	anbi2d	$⊢ (R Se A \land X \in A) \to ((\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X) \leftrightarrow (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land (y \in A \land y R X)))$
146	140 142 145	3bitr4rd	$⊢ (R Se A \land X \in A) \to ((\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X) \leftrightarrow y \in Pred (R, A, X))$
147		df-3an	$⊢ (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow ((f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜}))$
148		breq12	$⊢ (f (\emptyset) = y \land f (1_{𝑜}) = X) \to (f (\emptyset) ({R ↾}_{A}) f (1_{𝑜}) \leftrightarrow y ({R ↾}_{A}) X)$
149	148	adantl	$⊢ (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \to (f (\emptyset) ({R ↾}_{A}) f (1_{𝑜}) \leftrightarrow y ({R ↾}_{A}) X)$
150	149	pm5.32i	$⊢ ((f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow ((f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X)$
151	147 150	bitri	$⊢ (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow ((f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X)$
152	151	exbii	$⊢ \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow \exists f ((f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X)$
153		19.41v	$⊢ \exists f ((f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X) \leftrightarrow (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X)$
154	152 153	bitri	$⊢ \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X)$
155	154	a1i	$⊢ (R Se A \land X \in A) \to (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X)) \land y ({R ↾}_{A}) X))$
156	1	fveq1i	$⊢ F (\emptyset) = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset)$
157		setlikespec	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \in V$
158	157	ancoms	$⊢ (R Se A \land X \in A) \to Pred (R, A, X) \in V$
159		rdg0g	$⊢ Pred (R, A, X) \in V \to rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset) = Pred (R, A, X)$
160	158 159	syl	$⊢ (R Se A \land X \in A) \to rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X)) (\emptyset) = Pred (R, A, X)$
161	156 160	eqtrid	$⊢ (R Se A \land X \in A) \to F (\emptyset) = Pred (R, A, X)$
162	161	eleq2d	$⊢ (R Se A \land X \in A) \to (y \in F (\emptyset) \leftrightarrow y \in Pred (R, A, X))$
163	146 155 162	3bitr4d	$⊢ (R Se A \land X \in A) \to (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow y \in F (\emptyset))$
164	163	alrimiv	$⊢ (R Se A \land X \in A) \to \forall y (\exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = y \land f (1_{𝑜}) = X) \land f (\emptyset) ({R ↾}_{A}) f (1_{𝑜})) \leftrightarrow y \in F (\emptyset))$
165		eliun	$⊢ y \in ⋃_{z \in F (n)} Pred (R, A, z) \leftrightarrow \exists z \in F (n) y \in Pred (R, A, z)$
166		df-rex	$⊢ \exists z \in F (n) y \in Pred (R, A, z) \leftrightarrow \exists z (z \in F (n) \land y \in Pred (R, A, z))$
167	165 166	bitri	$⊢ y \in ⋃_{z \in F (n)} Pred (R, A, z) \leftrightarrow \exists z (z \in F (n) \land y \in Pred (R, A, z))$
168	101	elpred	$⊢ z \in V \to (y \in Pred (R, A, z) \leftrightarrow (y \in A \land y R z))$
169	168	elv	$⊢ y \in Pred (R, A, z) \leftrightarrow (y \in A \land y R z)$
170	169	anbi2i	$⊢ (z \in F (n) \land y \in Pred (R, A, z)) \leftrightarrow (z \in F (n) \land (y \in A \land y R z))$
171		anbi1	$⊢ (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n)) \to ((\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)) \leftrightarrow (z \in F (n) \land (y \in A \land y R z)))$
172	170 171	bitr4id	$⊢ (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n)) \to ((z \in F (n) \land y \in Pred (R, A, z)) \leftrightarrow (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
173	172	alexbii	$⊢ \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n)) \to (\exists z (z \in F (n) \land y \in Pred (R, A, z)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
174	173	3ad2ant3	$⊢ (n \in ω \land (R Se A \land X \in A) \land \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))) \to (\exists z (z \in F (n) \land y \in Pred (R, A, z)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
175	167 174	syl5bb	$⊢ (n \in ω \land (R Se A \land X \in A) \land \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))) \to (y \in ⋃_{z \in F (n)} Pred (R, A, z) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
176		nnon	$⊢ n \in ω \to n \in On$
177		fvex	$⊢ F (n) \in V$
178	1	ttrclselem1	$⊢ n \in ω \to F (n) \subseteq A$
179	178	adantr	$⊢ (n \in ω \land R Se A) \to F (n) \subseteq A$
180		dfse3	$⊢ R Se A \leftrightarrow \forall z \in A Pred (R, A, z) \in V$
181	180	biimpi	$⊢ R Se A \to \forall z \in A Pred (R, A, z) \in V$
182	181	adantl	$⊢ (n \in ω \land R Se A) \to \forall z \in A Pred (R, A, z) \in V$
183		ssralv	$⊢ F (n) \subseteq A \to (\forall z \in A Pred (R, A, z) \in V \to \forall z \in F (n) Pred (R, A, z) \in V)$
184	179 182 183	sylc	$⊢ (n \in ω \land R Se A) \to \forall z \in F (n) Pred (R, A, z) \in V$
185	184	adantrr	$⊢ (n \in ω \land (R Se A \land X \in A)) \to \forall z \in F (n) Pred (R, A, z) \in V$
186		iunexg	$⊢ (F (n) \in V \land \forall z \in F (n) Pred (R, A, z) \in V) \to ⋃_{z \in F (n)} Pred (R, A, z) \in V$
187	177 185 186	sylancr	$⊢ (n \in ω \land (R Se A \land X \in A)) \to ⋃_{z \in F (n)} Pred (R, A, z) \in V$
188		nfcv	$⊢ \underline{Ⅎ} b Pred (R, A, X)$
189		nfcv	$⊢ \underline{Ⅎ} b n$
190		nfmpt1	$⊢ \underline{Ⅎ} b (b \in V ⟼ ⋃_{w \in b} Pred (R, A, w))$
191	190 188	nfrdg	$⊢ \underline{Ⅎ} b rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X))$
192	1 191	nfcxfr	$⊢ \underline{Ⅎ} b F$
193	192 189	nffv	$⊢ \underline{Ⅎ} b F (n)$
194		nfcv	$⊢ \underline{Ⅎ} b Pred (R, A, z)$
195	193 194	nfiun	$⊢ \underline{Ⅎ} b ⋃_{z \in F (n)} Pred (R, A, z)$
196		predeq3	$⊢ w = z \to Pred (R, A, w) = Pred (R, A, z)$
197	196	cbviunv	$⊢ ⋃_{w \in b} Pred (R, A, w) = ⋃_{z \in b} Pred (R, A, z)$
198		iuneq1	$⊢ b = F (n) \to ⋃_{z \in b} Pred (R, A, z) = ⋃_{z \in F (n)} Pred (R, A, z)$
199	197 198	eqtrid	$⊢ b = F (n) \to ⋃_{w \in b} Pred (R, A, w) = ⋃_{z \in F (n)} Pred (R, A, z)$
200	188 189 195 1 199	rdgsucmptf	$⊢ (n \in On \land ⋃_{z \in F (n)} Pred (R, A, z) \in V) \to F (suc n) = ⋃_{z \in F (n)} Pred (R, A, z)$
201	176 187 200	syl2an2r	$⊢ (n \in ω \land (R Se A \land X \in A)) \to F (suc n) = ⋃_{z \in F (n)} Pred (R, A, z)$
202	201	3adant3	$⊢ (n \in ω \land (R Se A \land X \in A) \land \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))) \to F (suc n) = ⋃_{z \in F (n)} Pred (R, A, z)$
203	202	eleq2d	$⊢ (n \in ω \land (R Se A \land X \in A) \land \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))) \to (y \in F (suc n) \leftrightarrow y \in ⋃_{z \in F (n)} Pred (R, A, z))$
204		eqeq2	$⊢ x = X \to (f (suc suc n) = x \leftrightarrow f (suc suc n) = X)$
205	204	anbi2d	$⊢ x = X \to ((f (\emptyset) = y \land f (suc suc n) = x) \leftrightarrow (f (\emptyset) = y \land f (suc suc n) = X))$
206	205	3anbi2d	$⊢ x = X \to ((f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)))$
207	206	exbidv	$⊢ x = X \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)))$
208		eqeq2	$⊢ x = X \to (g (suc n) = x \leftrightarrow g (suc n) = X)$
209	208	anbi2d	$⊢ x = X \to ((g (\emptyset) = z \land g (suc n) = x) \leftrightarrow (g (\emptyset) = z \land g (suc n) = X))$
210	209	3anbi2d	$⊢ x = X \to ((g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)))$
211	210	exbidv	$⊢ x = X \to (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow \exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)))$
212	211	anbi1d	$⊢ x = X \to ((\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)) \leftrightarrow (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
213	212	exbidv	$⊢ x = X \to (\exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
214	207 213	bibi12d	$⊢ x = X \to ((\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z))) \leftrightarrow (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z))))$
215	214	imbi2d	$⊢ x = X \to ((n \in ω \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))) \leftrightarrow (n \in ω \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))))$
216		fvex	$⊢ f (suc b) \in V$
217		eqid	$⊢ (b \in suc suc n ⟼ f (suc b)) = (b \in suc suc n ⟼ f (suc b))$
218	216 217	fnmpti	$⊢ (b \in suc suc n ⟼ f (suc b)) Fn suc suc n$
219	218	a1i	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to (b \in suc suc n ⟼ f (suc b)) Fn suc suc n$
220		peano2	$⊢ n \in ω \to suc n \in ω$
221	220	adantr	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to suc n \in ω$
222		nnord	$⊢ suc n \in ω \to Ord suc n$
223	221 222	syl	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to Ord suc n$
224		0elsuc	$⊢ Ord suc n \to \emptyset \in suc suc n$
225	223 224	syl	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to \emptyset \in suc suc n$
226		suceq	$⊢ b = \emptyset \to suc b = suc \emptyset$
227	226	fveq2d	$⊢ b = \emptyset \to f (suc b) = f (suc \emptyset)$
228		fvex	$⊢ f (suc \emptyset) \in V$
229	227 217 228	fvmpt	$⊢ \emptyset \in suc suc n \to (b \in suc suc n ⟼ f (suc b)) (\emptyset) = f (suc \emptyset)$
230	225 229	syl	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to (b \in suc suc n ⟼ f (suc b)) (\emptyset) = f (suc \emptyset)$
231		vex	$⊢ n \in V$
232	231	sucex	$⊢ suc n \in V$
233	232	sucid	$⊢ suc n \in suc suc n$
234		suceq	$⊢ b = suc n \to suc b = suc suc n$
235	234	fveq2d	$⊢ b = suc n \to f (suc b) = f (suc suc n)$
236		fvex	$⊢ f (suc suc n) \in V$
237	235 217 236	fvmpt	$⊢ suc n \in suc suc n \to (b \in suc suc n ⟼ f (suc b)) (suc n) = f (suc suc n)$
238	233 237	mp1i	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to (b \in suc suc n ⟼ f (suc b)) (suc n) = f (suc suc n)$
239		simpr2r	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to f (suc suc n) = x$
240	238 239	eqtrd	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to (b \in suc suc n ⟼ f (suc b)) (suc n) = x$
241		fveq2	$⊢ a = suc c \to f (a) = f (suc c)$
242		suceq	$⊢ a = suc c \to suc a = suc suc c$
243	242	fveq2d	$⊢ a = suc c \to f (suc a) = f (suc suc c)$
244	241 243	breq12d	$⊢ a = suc c \to (f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow f (suc c) ({R ↾}_{A}) f (suc suc c))$
245		simplr3	$⊢ ((n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \land c \in suc n) \to \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)$
246		ordsucelsuc	$⊢ Ord suc n \to (c \in suc n \leftrightarrow suc c \in suc suc n)$
247	223 246	syl	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to (c \in suc n \leftrightarrow suc c \in suc suc n)$
248	247	biimpa	$⊢ ((n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \land c \in suc n) \to suc c \in suc suc n$
249	244 245 248	rspcdva	$⊢ ((n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \land c \in suc n) \to f (suc c) ({R ↾}_{A}) f (suc suc c)$
250		elelsuc	$⊢ c \in suc n \to c \in suc suc n$
251		suceq	$⊢ b = c \to suc b = suc c$
252	251	fveq2d	$⊢ b = c \to f (suc b) = f (suc c)$
253		fvex	$⊢ f (suc c) \in V$
254	252 217 253	fvmpt	$⊢ c \in suc suc n \to (b \in suc suc n ⟼ f (suc b)) (c) = f (suc c)$
255	250 254	syl	$⊢ c \in suc n \to (b \in suc suc n ⟼ f (suc b)) (c) = f (suc c)$
256	255	adantl	$⊢ ((n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \land c \in suc n) \to (b \in suc suc n ⟼ f (suc b)) (c) = f (suc c)$
257		suceq	$⊢ b = suc c \to suc b = suc suc c$
258	257	fveq2d	$⊢ b = suc c \to f (suc b) = f (suc suc c)$
259		fvex	$⊢ f (suc suc c) \in V$
260	258 217 259	fvmpt	$⊢ suc c \in suc suc n \to (b \in suc suc n ⟼ f (suc b)) (suc c) = f (suc suc c)$
261	248 260	syl	$⊢ ((n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \land c \in suc n) \to (b \in suc suc n ⟼ f (suc b)) (suc c) = f (suc suc c)$
262	249 256 261	3brtr4d	$⊢ ((n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \land c \in suc n) \to (b \in suc suc n ⟼ f (suc b)) (c) ({R ↾}_{A}) (b \in suc suc n ⟼ f (suc b)) (suc c)$
263	262	ralrimiva	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to \forall c \in suc n (b \in suc suc n ⟼ f (suc b)) (c) ({R ↾}_{A}) (b \in suc suc n ⟼ f (suc b)) (suc c)$
264	232	sucex	$⊢ suc suc n \in V$
265	264	mptex	$⊢ (b \in suc suc n ⟼ f (suc b)) \in V$
266		fneq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to (g Fn suc suc n \leftrightarrow (b \in suc suc n ⟼ f (suc b)) Fn suc suc n)$
267		fveq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to g (\emptyset) = (b \in suc suc n ⟼ f (suc b)) (\emptyset)$
268	267	eqeq1d	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to (g (\emptyset) = f (suc \emptyset) \leftrightarrow (b \in suc suc n ⟼ f (suc b)) (\emptyset) = f (suc \emptyset))$
269		fveq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to g (suc n) = (b \in suc suc n ⟼ f (suc b)) (suc n)$
270	269	eqeq1d	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to (g (suc n) = x \leftrightarrow (b \in suc suc n ⟼ f (suc b)) (suc n) = x)$
271	268 270	anbi12d	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to ((g (\emptyset) = f (suc \emptyset) \land g (suc n) = x) \leftrightarrow ((b \in suc suc n ⟼ f (suc b)) (\emptyset) = f (suc \emptyset) \land (b \in suc suc n ⟼ f (suc b)) (suc n) = x))$
272		fveq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to g (c) = (b \in suc suc n ⟼ f (suc b)) (c)$
273		fveq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to g (suc c) = (b \in suc suc n ⟼ f (suc b)) (suc c)$
274	272 273	breq12d	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to (g (c) ({R ↾}_{A}) g (suc c) \leftrightarrow (b \in suc suc n ⟼ f (suc b)) (c) ({R ↾}_{A}) (b \in suc suc n ⟼ f (suc b)) (suc c))$
275	274	ralbidv	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to (\forall c \in suc n g (c) ({R ↾}_{A}) g (suc c) \leftrightarrow \forall c \in suc n (b \in suc suc n ⟼ f (suc b)) (c) ({R ↾}_{A}) (b \in suc suc n ⟼ f (suc b)) (suc c))$
276	266 271 275	3anbi123d	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to ((g Fn suc suc n \land (g (\emptyset) = f (suc \emptyset) \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow ((b \in suc suc n ⟼ f (suc b)) Fn suc suc n \land ((b \in suc suc n ⟼ f (suc b)) (\emptyset) = f (suc \emptyset) \land (b \in suc suc n ⟼ f (suc b)) (suc n) = x) \land \forall c \in suc n (b \in suc suc n ⟼ f (suc b)) (c) ({R ↾}_{A}) (b \in suc suc n ⟼ f (suc b)) (suc c)))$
277	265 276	spcev	$⊢ ((b \in suc suc n ⟼ f (suc b)) Fn suc suc n \land ((b \in suc suc n ⟼ f (suc b)) (\emptyset) = f (suc \emptyset) \land (b \in suc suc n ⟼ f (suc b)) (suc n) = x) \land \forall c \in suc n (b \in suc suc n ⟼ f (suc b)) (c) ({R ↾}_{A}) (b \in suc suc n ⟼ f (suc b)) (suc c)) \to \exists g (g Fn suc suc n \land (g (\emptyset) = f (suc \emptyset) \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c))$
278	219 230 240 263 277	syl121anc	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to \exists g (g Fn suc suc n \land (g (\emptyset) = f (suc \emptyset) \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c))$
279		simpr2l	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to f (\emptyset) = y$
280	15	fveq2d	$⊢ a = \emptyset \to f (suc a) = f (suc \emptyset)$
281	14 280	breq12d	$⊢ a = \emptyset \to (f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow f (\emptyset) ({R ↾}_{A}) f (suc \emptyset))$
282		simpr3	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)$
283	281 282 225	rspcdva	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to f (\emptyset) ({R ↾}_{A}) f (suc \emptyset)$
284	279 283	eqbrtrrd	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to y ({R ↾}_{A}) f (suc \emptyset)$
285		eqeq2	$⊢ z = f (suc \emptyset) \to (g (\emptyset) = z \leftrightarrow g (\emptyset) = f (suc \emptyset))$
286	285	anbi1d	$⊢ z = f (suc \emptyset) \to ((g (\emptyset) = z \land g (suc n) = x) \leftrightarrow (g (\emptyset) = f (suc \emptyset) \land g (suc n) = x))$
287	286	3anbi2d	$⊢ z = f (suc \emptyset) \to ((g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow (g Fn suc suc n \land (g (\emptyset) = f (suc \emptyset) \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)))$
288	287	exbidv	$⊢ z = f (suc \emptyset) \to (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow \exists g (g Fn suc suc n \land (g (\emptyset) = f (suc \emptyset) \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)))$
289		breq2	$⊢ z = f (suc \emptyset) \to (y ({R ↾}_{A}) z \leftrightarrow y ({R ↾}_{A}) f (suc \emptyset))$
290	288 289	anbi12d	$⊢ z = f (suc \emptyset) \to ((\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \leftrightarrow (\exists g (g Fn suc suc n \land (g (\emptyset) = f (suc \emptyset) \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) f (suc \emptyset)))$
291	228 290	spcev	$⊢ (\exists g (g Fn suc suc n \land (g (\emptyset) = f (suc \emptyset) \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) f (suc \emptyset)) \to \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z)$
292	278 284 291	syl2anc	$⊢ (n \in ω \land (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))) \to \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z)$
293	292	ex	$⊢ n \in ω \to ((f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \to \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z))$
294	293	exlimdv	$⊢ n \in ω \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \to \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z))$
295		fvex	$⊢ g (⋃ b) \in V$
296	101 295	ifex	$⊢ if (b = \emptyset, y, g (⋃ b)) \in V$
297		eqid	$⊢ (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b)))$
298	296 297	fnmpti	$⊢ (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) Fn suc suc suc n$
299	298	a1i	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) Fn suc suc suc n$
300		peano2	$⊢ suc n \in ω \to suc suc n \in ω$
301	220 300	syl	$⊢ n \in ω \to suc suc n \in ω$
302	301	3ad2ant1	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to suc suc n \in ω$
303		nnord	$⊢ suc suc n \in ω \to Ord suc suc n$
304	302 303	syl	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to Ord suc suc n$
305		0elsuc	$⊢ Ord suc suc n \to \emptyset \in suc suc suc n$
306	304 305	syl	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to \emptyset \in suc suc suc n$
307		iftrue	$⊢ b = \emptyset \to if (b = \emptyset, y, g (⋃ b)) = y$
308	307 297 101	fvmpt	$⊢ \emptyset \in suc suc suc n \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (\emptyset) = y$
309	306 308	syl	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (\emptyset) = y$
310	264	sucid	$⊢ suc suc n \in suc suc suc n$
311		eqeq1	$⊢ b = suc suc n \to (b = \emptyset \leftrightarrow suc suc n = \emptyset)$
312		unieq	$⊢ b = suc suc n \to ⋃ b = ⋃ suc suc n$
313	312	fveq2d	$⊢ b = suc suc n \to g (⋃ b) = g (⋃ suc suc n)$
314	311 313	ifbieq2d	$⊢ b = suc suc n \to if (b = \emptyset, y, g (⋃ b)) = if (suc suc n = \emptyset, y, g (⋃ suc suc n))$
315		nsuceq0	$⊢ suc suc n \neq \emptyset$
316	315	neii	$⊢ \neg suc suc n = \emptyset$
317	316	iffalsei	$⊢ if (suc suc n = \emptyset, y, g (⋃ suc suc n)) = g (⋃ suc suc n)$
318	314 317	eqtrdi	$⊢ b = suc suc n \to if (b = \emptyset, y, g (⋃ b)) = g (⋃ suc suc n)$
319		fvex	$⊢ g (⋃ suc suc n) \in V$
320	318 297 319	fvmpt	$⊢ suc suc n \in suc suc suc n \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc suc n) = g (⋃ suc suc n)$
321	310 320	mp1i	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc suc n) = g (⋃ suc suc n)$
322	220	3ad2ant1	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to suc n \in ω$
323	322 222	syl	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to Ord suc n$
324		ordunisuc	$⊢ Ord suc n \to ⋃ suc suc n = suc n$
325	323 324	syl	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to ⋃ suc suc n = suc n$
326	325	fveq2d	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to g (⋃ suc suc n) = g (suc n)$
327		simp22r	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to g (suc n) = x$
328	321 326 327	3eqtrd	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc suc n) = x$
329		simpl3	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a = \emptyset) \to y ({R ↾}_{A}) z$
330		iftrue	$⊢ a = \emptyset \to if (a = \emptyset, y, g (⋃ a)) = y$
331	330	adantl	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a = \emptyset) \to if (a = \emptyset, y, g (⋃ a)) = y$
332		fveq2	$⊢ a = \emptyset \to g (a) = g (\emptyset)$
333		simp22l	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to g (\emptyset) = z$
334	332 333	sylan9eqr	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a = \emptyset) \to g (a) = z$
335	329 331 334	3brtr4d	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a = \emptyset) \to if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a)$
336	335	ex	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (a = \emptyset \to if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a))$
337	336	adantr	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to (a = \emptyset \to if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a))$
338		ordsucelsuc	$⊢ Ord suc n \to (b \in suc n \leftrightarrow suc b \in suc suc n)$
339	323 338	syl	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (b \in suc n \leftrightarrow suc b \in suc suc n)$
340		elnn	$⊢ (b \in suc n \land suc n \in ω) \to b \in ω$
341	322 340	sylan2	$⊢ (b \in suc n \land (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z)) \to b \in ω$
342	341	ancoms	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land b \in suc n) \to b \in ω$
343		nnord	$⊢ b \in ω \to Ord b$
344	342 343	syl	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land b \in suc n) \to Ord b$
345		ordunisuc	$⊢ Ord b \to ⋃ suc b = b$
346	344 345	syl	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land b \in suc n) \to ⋃ suc b = b$
347	346	fveq2d	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land b \in suc n) \to g (⋃ suc b) = g (b)$
348		simp23	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)$
349		fveq2	$⊢ c = b \to g (c) = g (b)$
350		suceq	$⊢ c = b \to suc c = suc b$
351	350	fveq2d	$⊢ c = b \to g (suc c) = g (suc b)$
352	349 351	breq12d	$⊢ c = b \to (g (c) ({R ↾}_{A}) g (suc c) \leftrightarrow g (b) ({R ↾}_{A}) g (suc b))$
353	352	rspcv	$⊢ b \in suc n \to (\forall c \in suc n g (c) ({R ↾}_{A}) g (suc c) \to g (b) ({R ↾}_{A}) g (suc b))$
354	348 353	mpan9	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land b \in suc n) \to g (b) ({R ↾}_{A}) g (suc b)$
355	347 354	eqbrtrd	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land b \in suc n) \to g (⋃ suc b) ({R ↾}_{A}) g (suc b)$
356	355	ex	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (b \in suc n \to g (⋃ suc b) ({R ↾}_{A}) g (suc b))$
357	339 356	sylbird	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (suc b \in suc suc n \to g (⋃ suc b) ({R ↾}_{A}) g (suc b))$
358	357	imp	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land suc b \in suc suc n) \to g (⋃ suc b) ({R ↾}_{A}) g (suc b)$
359		eleq1	$⊢ a = suc b \to (a \in suc suc n \leftrightarrow suc b \in suc suc n)$
360	359	anbi2d	$⊢ a = suc b \to (((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \leftrightarrow ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land suc b \in suc suc n))$
361		eqeq1	$⊢ a = suc b \to (a = \emptyset \leftrightarrow suc b = \emptyset)$
362		unieq	$⊢ a = suc b \to ⋃ a = ⋃ suc b$
363	362	fveq2d	$⊢ a = suc b \to g (⋃ a) = g (⋃ suc b)$
364	361 363	ifbieq2d	$⊢ a = suc b \to if (a = \emptyset, y, g (⋃ a)) = if (suc b = \emptyset, y, g (⋃ suc b))$
365		nsuceq0	$⊢ suc b \neq \emptyset$
366	365	neii	$⊢ \neg suc b = \emptyset$
367	366	iffalsei	$⊢ if (suc b = \emptyset, y, g (⋃ suc b)) = g (⋃ suc b)$
368	364 367	eqtrdi	$⊢ a = suc b \to if (a = \emptyset, y, g (⋃ a)) = g (⋃ suc b)$
369		fveq2	$⊢ a = suc b \to g (a) = g (suc b)$
370	368 369	breq12d	$⊢ a = suc b \to (if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a) \leftrightarrow g (⋃ suc b) ({R ↾}_{A}) g (suc b))$
371	360 370	imbi12d	$⊢ a = suc b \to ((((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a)) \leftrightarrow (((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land suc b \in suc suc n) \to g (⋃ suc b) ({R ↾}_{A}) g (suc b)))$
372	358 371	mpbiri	$⊢ a = suc b \to (((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a))$
373	372	com12	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to (a = suc b \to if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a))$
374	373	rexlimdvw	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to (\exists b \in ω a = suc b \to if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a))$
375		elnn	$⊢ (a \in suc suc n \land suc suc n \in ω) \to a \in ω$
376	375	ancoms	$⊢ (suc suc n \in ω \land a \in suc suc n) \to a \in ω$
377	302 376	sylan	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to a \in ω$
378		nn0suc	$⊢ a \in ω \to (a = \emptyset \lor \exists b \in ω a = suc b)$
379	377 378	syl	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to (a = \emptyset \lor \exists b \in ω a = suc b)$
380	337 374 379	mpjaod	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a)$
381		elelsuc	$⊢ a \in suc suc n \to a \in suc suc suc n$
382		eqeq1	$⊢ b = a \to (b = \emptyset \leftrightarrow a = \emptyset)$
383		unieq	$⊢ b = a \to ⋃ b = ⋃ a$
384	383	fveq2d	$⊢ b = a \to g (⋃ b) = g (⋃ a)$
385	382 384	ifbieq2d	$⊢ b = a \to if (b = \emptyset, y, g (⋃ b)) = if (a = \emptyset, y, g (⋃ a))$
386		fvex	$⊢ g (⋃ a) \in V$
387	101 386	ifex	$⊢ if (a = \emptyset, y, g (⋃ a)) \in V$
388	385 297 387	fvmpt	$⊢ a \in suc suc suc n \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) = if (a = \emptyset, y, g (⋃ a))$
389	381 388	syl	$⊢ a \in suc suc n \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) = if (a = \emptyset, y, g (⋃ a))$
390	389	adantl	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) = if (a = \emptyset, y, g (⋃ a))$
391		ordsucelsuc	$⊢ Ord suc suc n \to (a \in suc suc n \leftrightarrow suc a \in suc suc suc n)$
392	304 391	syl	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to (a \in suc suc n \leftrightarrow suc a \in suc suc suc n)$
393	392	biimpa	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to suc a \in suc suc suc n$
394		eqeq1	$⊢ b = suc a \to (b = \emptyset \leftrightarrow suc a = \emptyset)$
395		unieq	$⊢ b = suc a \to ⋃ b = ⋃ suc a$
396	395	fveq2d	$⊢ b = suc a \to g (⋃ b) = g (⋃ suc a)$
397	394 396	ifbieq2d	$⊢ b = suc a \to if (b = \emptyset, y, g (⋃ b)) = if (suc a = \emptyset, y, g (⋃ suc a))$
398		nsuceq0	$⊢ suc a \neq \emptyset$
399	398	neii	$⊢ \neg suc a = \emptyset$
400	399	iffalsei	$⊢ if (suc a = \emptyset, y, g (⋃ suc a)) = g (⋃ suc a)$
401	397 400	eqtrdi	$⊢ b = suc a \to if (b = \emptyset, y, g (⋃ b)) = g (⋃ suc a)$
402		fvex	$⊢ g (⋃ suc a) \in V$
403	401 297 402	fvmpt	$⊢ suc a \in suc suc suc n \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a) = g (⋃ suc a)$
404	393 403	syl	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a) = g (⋃ suc a)$
405		nnord	$⊢ a \in ω \to Ord a$
406	377 405	syl	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to Ord a$
407		ordunisuc	$⊢ Ord a \to ⋃ suc a = a$
408	406 407	syl	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to ⋃ suc a = a$
409	408	fveq2d	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to g (⋃ suc a) = g (a)$
410	404 409	eqtrd	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a) = g (a)$
411	380 390 410	3brtr4d	$⊢ ((n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \land a \in suc suc n) \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) ({R ↾}_{A}) (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a)$
412	411	ralrimiva	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to \forall a \in suc suc n (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) ({R ↾}_{A}) (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a)$
413	264	sucex	$⊢ suc suc suc n \in V$
414	413	mptex	$⊢ (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \in V$
415		fneq1	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to (f Fn suc suc suc n \leftrightarrow (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) Fn suc suc suc n)$
416		fveq1	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to f (\emptyset) = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (\emptyset)$
417	416	eqeq1d	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to (f (\emptyset) = y \leftrightarrow (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (\emptyset) = y)$
418		fveq1	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to f (suc suc n) = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc suc n)$
419	418	eqeq1d	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to (f (suc suc n) = x \leftrightarrow (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc suc n) = x)$
420	417 419	anbi12d	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to ((f (\emptyset) = y \land f (suc suc n) = x) \leftrightarrow ((b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (\emptyset) = y \land (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc suc n) = x))$
421		fveq1	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to f (a) = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a)$
422		fveq1	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to f (suc a) = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a)$
423	421 422	breq12d	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to (f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) ({R ↾}_{A}) (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a))$
424	423	ralbidv	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to (\forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow \forall a \in suc suc n (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) ({R ↾}_{A}) (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a))$
425	415 420 424	3anbi123d	$⊢ f = (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \to ((f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow ((b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) Fn suc suc suc n \land ((b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (\emptyset) = y \land (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc suc n) = x) \land \forall a \in suc suc n (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) ({R ↾}_{A}) (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a)))$
426	414 425	spcev	$⊢ ((b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) Fn suc suc suc n \land ((b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (\emptyset) = y \land (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc suc n) = x) \land \forall a \in suc suc n (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (a) ({R ↾}_{A}) (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (suc a)) \to \exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))$
427	299 309 328 412 426	syl121anc	$⊢ (n \in ω \land (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to \exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))$
428	427	3exp	$⊢ n \in ω \to ((g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \to (y ({R ↾}_{A}) z \to \exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))))$
429	428	exlimdv	$⊢ n \in ω \to (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \to (y ({R ↾}_{A}) z \to \exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a))))$
430	429	impd	$⊢ n \in ω \to ((\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to \exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)))$
431	430	exlimdv	$⊢ n \in ω \to (\exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \to \exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)))$
432	294 431	impbid	$⊢ n \in ω \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z))$
433		vex	$⊢ z \in V$
434	433	brresi	$⊢ y ({R ↾}_{A}) z \leftrightarrow (y \in A \land y R z)$
435	434	anbi2i	$⊢ (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \leftrightarrow (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z))$
436	435	exbii	$⊢ \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land y ({R ↾}_{A}) z) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z))$
437	432 436	bitrdi	$⊢ n \in ω \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = x) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = x) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
438	215 437	vtoclg	$⊢ X \in A \to (n \in ω \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z))))$
439	438	impcom	$⊢ (n \in ω \land X \in A) \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
440	439	adantrl	$⊢ (n \in ω \land (R Se A \land X \in A)) \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
441	440	3adant3	$⊢ (n \in ω \land (R Se A \land X \in A) \land \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))) \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \land (y \in A \land y R z)))$
442	175 203 441	3bitr4rd	$⊢ (n \in ω \land (R Se A \land X \in A) \land \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))) \to (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (suc n))$
443	442	alrimiv	$⊢ (n \in ω \land (R Se A \land X \in A) \land \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))) \to \forall y (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (suc n))$
444	443	3exp	$⊢ n \in ω \to ((R Se A \land X \in A) \to (\forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n)) \to \forall y (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (suc n))))$
445	444	a2d	$⊢ n \in ω \to (((R Se A \land X \in A) \to \forall z (\exists g (g Fn suc suc n \land (g (\emptyset) = z \land g (suc n) = X) \land \forall c \in suc n g (c) ({R ↾}_{A}) g (suc c)) \leftrightarrow z \in F (n))) \to ((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc suc n \land (f (\emptyset) = y \land f (suc suc n) = X) \land \forall a \in suc suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (suc n))))$
446	27 68 82 96 164 445	finds	$⊢ N \in ω \to ((R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (N)))$
447	446	3impib	$⊢ (N \in ω \land R Se A \land X \in A) \to \forall y (\exists f (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (N))$
448	447	19.21bi	$⊢ (N \in ω \land R Se A \land X \in A) \to (\exists f (f Fn suc suc N \land (f (\emptyset) = y \land f (suc N) = X) \land \forall a \in suc N f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in F (N))$

Metamath Proof Explorer

Theorem ttrclselem2

Proof