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	bitrid	$⊢ (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	bilani	$⊢ (n \in ω \land R Se A) \to \forall z \in A Pred (R, A, z) \in V$
182		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)$
183	179 181 182	sylc	$⊢ (n \in ω \land R Se A) \to \forall z \in F (n) Pred (R, A, z) \in V$
184	183	adantrr	$⊢ (n \in ω \land (R Se A \land X \in A)) \to \forall z \in F (n) Pred (R, A, z) \in V$
185		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$
186	177 184 185	sylancr	$⊢ (n \in ω \land (R Se A \land X \in A)) \to ⋃_{z \in F (n)} Pred (R, A, z) \in V$
187		nfcv	$⊢ \underline{Ⅎ} b Pred (R, A, X)$
188		nfcv	$⊢ \underline{Ⅎ} b n$
189		nfmpt1	$⊢ \underline{Ⅎ} b (b \in V ⟼ ⋃_{w \in b} Pred (R, A, w))$
190	189 187	nfrdg	$⊢ \underline{Ⅎ} b rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, X))$
191	1 190	nfcxfr	$⊢ \underline{Ⅎ} b F$
192	191 188	nffv	$⊢ \underline{Ⅎ} b F (n)$
193		nfcv	$⊢ \underline{Ⅎ} b Pred (R, A, z)$
194	192 193	nfiun	$⊢ \underline{Ⅎ} b ⋃_{z \in F (n)} Pred (R, A, z)$
195		predeq3	$⊢ w = z \to Pred (R, A, w) = Pred (R, A, z)$
196	195	cbviunv	$⊢ ⋃_{w \in b} Pred (R, A, w) = ⋃_{z \in b} Pred (R, A, z)$
197		iuneq1	$⊢ b = F (n) \to ⋃_{z \in b} Pred (R, A, z) = ⋃_{z \in F (n)} Pred (R, A, z)$
198	196 197	eqtrid	$⊢ b = F (n) \to ⋃_{w \in b} Pred (R, A, w) = ⋃_{z \in F (n)} Pred (R, A, z)$
199	187 188 194 1 198	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)$
200	176 186 199	syl2an2r	$⊢ (n \in ω \land (R Se A \land X \in A)) \to F (suc n) = ⋃_{z \in F (n)} Pred (R, A, z)$
201	200	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)$
202	201	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))$
203		eqeq2	$⊢ x = X \to (f (suc suc n) = x \leftrightarrow f (suc suc n) = X)$
204	203	anbi2d	$⊢ x = X \to ((f (\emptyset) = y \land f (suc suc n) = x) \leftrightarrow (f (\emptyset) = y \land f (suc suc n) = X))$
205	204	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)))$
206	205	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)))$
207		eqeq2	$⊢ x = X \to (g (suc n) = x \leftrightarrow g (suc n) = X)$
208	207	anbi2d	$⊢ x = X \to ((g (\emptyset) = z \land g (suc n) = x) \leftrightarrow (g (\emptyset) = z \land g (suc n) = X))$
209	208	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)))$
210	209	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)))$
211	210	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)))$
212	211	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)))$
213	206 212	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))))$
214	213	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)))))$
215		fvex	$⊢ f (suc b) \in V$
216		eqid	$⊢ (b \in suc suc n ⟼ f (suc b)) = (b \in suc suc n ⟼ f (suc b))$
217	215 216	fnmpti	$⊢ (b \in suc suc n ⟼ f (suc b)) Fn suc suc n$
218	217	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$
219		peano2	$⊢ n \in ω \to suc n \in ω$
220	219	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 ω$
221		nnord	$⊢ suc n \in ω \to Ord suc n$
222	220 221	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$
223		0elsuc	$⊢ Ord suc n \to \emptyset \in suc suc n$
224	222 223	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$
225		suceq	$⊢ b = \emptyset \to suc b = suc \emptyset$
226	225	fveq2d	$⊢ b = \emptyset \to f (suc b) = f (suc \emptyset)$
227		fvex	$⊢ f (suc \emptyset) \in V$
228	226 216 227	fvmpt	$⊢ \emptyset \in suc suc n \to (b \in suc suc n ⟼ f (suc b)) (\emptyset) = f (suc \emptyset)$
229	224 228	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)$
230		vex	$⊢ n \in V$
231	230	sucex	$⊢ suc n \in V$
232	231	sucid	$⊢ suc n \in suc suc n$
233		suceq	$⊢ b = suc n \to suc b = suc suc n$
234	233	fveq2d	$⊢ b = suc n \to f (suc b) = f (suc suc n)$
235		fvex	$⊢ f (suc suc n) \in V$
236	234 216 235	fvmpt	$⊢ suc n \in suc suc n \to (b \in suc suc n ⟼ f (suc b)) (suc n) = f (suc suc n)$
237	232 236	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)$
238		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$
239	237 238	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$
240		fveq2	$⊢ a = suc c \to f (a) = f (suc c)$
241		suceq	$⊢ a = suc c \to suc a = suc suc c$
242	241	fveq2d	$⊢ a = suc c \to f (suc a) = f (suc suc c)$
243	240 242	breq12d	$⊢ a = suc c \to (f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow f (suc c) ({R ↾}_{A}) f (suc suc c))$
244		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)$
245		ordsucelsuc	$⊢ Ord suc n \to (c \in suc n \leftrightarrow suc c \in suc suc n)$
246	222 245	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)$
247	246	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$
248	243 244 247	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)$
249		elelsuc	$⊢ c \in suc n \to c \in suc suc n$
250		suceq	$⊢ b = c \to suc b = suc c$
251	250	fveq2d	$⊢ b = c \to f (suc b) = f (suc c)$
252		fvex	$⊢ f (suc c) \in V$
253	251 216 252	fvmpt	$⊢ c \in suc suc n \to (b \in suc suc n ⟼ f (suc b)) (c) = f (suc c)$
254	249 253	syl	$⊢ c \in suc n \to (b \in suc suc n ⟼ f (suc b)) (c) = f (suc c)$
255	254	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)$
256		suceq	$⊢ b = suc c \to suc b = suc suc c$
257	256	fveq2d	$⊢ b = suc c \to f (suc b) = f (suc suc c)$
258		fvex	$⊢ f (suc suc c) \in V$
259	257 216 258	fvmpt	$⊢ suc c \in suc suc n \to (b \in suc suc n ⟼ f (suc b)) (suc c) = f (suc suc c)$
260	247 259	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)$
261	248 255 260	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)$
262	261	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)$
263	231	sucex	$⊢ suc suc n \in V$
264	263	mptex	$⊢ (b \in suc suc n ⟼ f (suc b)) \in V$
265		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)$
266		fveq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to g (\emptyset) = (b \in suc suc n ⟼ f (suc b)) (\emptyset)$
267	266	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))$
268		fveq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to g (suc n) = (b \in suc suc n ⟼ f (suc b)) (suc n)$
269	268	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)$
270	267 269	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))$
271		fveq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to g (c) = (b \in suc suc n ⟼ f (suc b)) (c)$
272		fveq1	$⊢ g = (b \in suc suc n ⟼ f (suc b)) \to g (suc c) = (b \in suc suc n ⟼ f (suc b)) (suc c)$
273	271 272	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))$
274	273	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))$
275	265 270 274	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)))$
276	264 275	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))$
277	218 229 239 262 276	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))$
278		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$
279	15	fveq2d	$⊢ a = \emptyset \to f (suc a) = f (suc \emptyset)$
280	14 279	breq12d	$⊢ a = \emptyset \to (f (a) ({R ↾}_{A}) f (suc a) \leftrightarrow f (\emptyset) ({R ↾}_{A}) f (suc \emptyset))$
281		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)$
282	280 281 224	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)$
283	278 282	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)$
284		eqeq2	$⊢ z = f (suc \emptyset) \to (g (\emptyset) = z \leftrightarrow g (\emptyset) = f (suc \emptyset))$
285	284	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))$
286	285	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)))$
287	286	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)))$
288		breq2	$⊢ z = f (suc \emptyset) \to (y ({R ↾}_{A}) z \leftrightarrow y ({R ↾}_{A}) f (suc \emptyset))$
289	287 288	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)))$
290	227 289	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)$
291	277 283 290	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)$
292	291	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))$
293	292	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))$
294		fvex	$⊢ g (⋃ b) \in V$
295	101 294	ifex	$⊢ if (b = \emptyset, y, g (⋃ b)) \in V$
296		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)))$
297	295 296	fnmpti	$⊢ (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) Fn suc suc suc n$
298	297	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$
299		peano2	$⊢ suc n \in ω \to suc suc n \in ω$
300	219 299	syl	$⊢ n \in ω \to suc suc n \in ω$
301	300	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 ω$
302		nnord	$⊢ suc suc n \in ω \to Ord suc suc n$
303	301 302	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$
304		0elsuc	$⊢ Ord suc suc n \to \emptyset \in suc suc suc n$
305	303 304	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$
306		iftrue	$⊢ b = \emptyset \to if (b = \emptyset, y, g (⋃ b)) = y$
307	306 296 101	fvmpt	$⊢ \emptyset \in suc suc suc n \to (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) (\emptyset) = y$
308	305 307	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$
309	263	sucid	$⊢ suc suc n \in suc suc suc n$
310		eqeq1	$⊢ b = suc suc n \to (b = \emptyset \leftrightarrow suc suc n = \emptyset)$
311		unieq	$⊢ b = suc suc n \to ⋃ b = ⋃ suc suc n$
312	311	fveq2d	$⊢ b = suc suc n \to g (⋃ b) = g (⋃ suc suc n)$
313	310 312	ifbieq2d	$⊢ b = suc suc n \to if (b = \emptyset, y, g (⋃ b)) = if (suc suc n = \emptyset, y, g (⋃ suc suc n))$
314		nsuceq0	$⊢ suc suc n \neq \emptyset$
315	314	neii	$⊢ \neg suc suc n = \emptyset$
316	315	iffalsei	$⊢ if (suc suc n = \emptyset, y, g (⋃ suc suc n)) = g (⋃ suc suc n)$
317	313 316	eqtrdi	$⊢ b = suc suc n \to if (b = \emptyset, y, g (⋃ b)) = g (⋃ suc suc n)$
318		fvex	$⊢ g (⋃ suc suc n) \in V$
319	317 296 318	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)$
320	309 319	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)$
321	219	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 ω$
322	321 221	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$
323		ordunisuc	$⊢ Ord suc n \to ⋃ suc suc n = suc n$
324	322 323	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$
325	324	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)$
326		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$
327	320 325 326	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$
328		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$
329		iftrue	$⊢ a = \emptyset \to if (a = \emptyset, y, g (⋃ a)) = y$
330	329	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$
331		fveq2	$⊢ a = \emptyset \to g (a) = g (\emptyset)$
332		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$
333	331 332	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$
334	328 330 333	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)$
335	334	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))$
336	335	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))$
337		ordsucelsuc	$⊢ Ord suc n \to (b \in suc n \leftrightarrow suc b \in suc suc n)$
338	322 337	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)$
339		elnn	$⊢ (b \in suc n \land suc n \in ω) \to b \in ω$
340	321 339	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 ω$
341	340	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 ω$
342		nnord	$⊢ b \in ω \to Ord b$
343	341 342	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$
344		ordunisuc	$⊢ Ord b \to ⋃ suc b = b$
345	343 344	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$
346	345	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)$
347		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)$
348		fveq2	$⊢ c = b \to g (c) = g (b)$
349		suceq	$⊢ c = b \to suc c = suc b$
350	349	fveq2d	$⊢ c = b \to g (suc c) = g (suc b)$
351	348 350	breq12d	$⊢ c = b \to (g (c) ({R ↾}_{A}) g (suc c) \leftrightarrow g (b) ({R ↾}_{A}) g (suc b))$
352	351	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))$
353	347 352	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)$
354	346 353	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)$
355	354	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))$
356	338 355	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))$
357	356	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)$
358		eleq1	$⊢ a = suc b \to (a \in suc suc n \leftrightarrow suc b \in suc suc n)$
359	358	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))$
360		eqeq1	$⊢ a = suc b \to (a = \emptyset \leftrightarrow suc b = \emptyset)$
361		unieq	$⊢ a = suc b \to ⋃ a = ⋃ suc b$
362	361	fveq2d	$⊢ a = suc b \to g (⋃ a) = g (⋃ suc b)$
363	360 362	ifbieq2d	$⊢ a = suc b \to if (a = \emptyset, y, g (⋃ a)) = if (suc b = \emptyset, y, g (⋃ suc b))$
364		nsuceq0	$⊢ suc b \neq \emptyset$
365	364	neii	$⊢ \neg suc b = \emptyset$
366	365	iffalsei	$⊢ if (suc b = \emptyset, y, g (⋃ suc b)) = g (⋃ suc b)$
367	363 366	eqtrdi	$⊢ a = suc b \to if (a = \emptyset, y, g (⋃ a)) = g (⋃ suc b)$
368		fveq2	$⊢ a = suc b \to g (a) = g (suc b)$
369	367 368	breq12d	$⊢ a = suc b \to (if (a = \emptyset, y, g (⋃ a)) ({R ↾}_{A}) g (a) \leftrightarrow g (⋃ suc b) ({R ↾}_{A}) g (suc b))$
370	359 369	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)))$
371	357 370	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))$
372	371	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))$
373	372	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))$
374		elnn	$⊢ (a \in suc suc n \land suc suc n \in ω) \to a \in ω$
375	374	ancoms	$⊢ (suc suc n \in ω \land a \in suc suc n) \to a \in ω$
376	301 375	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 ω$
377		nn0suc	$⊢ a \in ω \to (a = \emptyset \lor \exists b \in ω a = suc b)$
378	376 377	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)$
379	336 373 378	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)$
380		elelsuc	$⊢ a \in suc suc n \to a \in suc suc suc n$
381		eqeq1	$⊢ b = a \to (b = \emptyset \leftrightarrow a = \emptyset)$
382		unieq	$⊢ b = a \to ⋃ b = ⋃ a$
383	382	fveq2d	$⊢ b = a \to g (⋃ b) = g (⋃ a)$
384	381 383	ifbieq2d	$⊢ b = a \to if (b = \emptyset, y, g (⋃ b)) = if (a = \emptyset, y, g (⋃ a))$
385		fvex	$⊢ g (⋃ a) \in V$
386	101 385	ifex	$⊢ if (a = \emptyset, y, g (⋃ a)) \in V$
387	384 296 386	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))$
388	380 387	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))$
389	388	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))$
390		ordsucelsuc	$⊢ Ord suc suc n \to (a \in suc suc n \leftrightarrow suc a \in suc suc suc n)$
391	303 390	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)$
392	391	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$
393		eqeq1	$⊢ b = suc a \to (b = \emptyset \leftrightarrow suc a = \emptyset)$
394		unieq	$⊢ b = suc a \to ⋃ b = ⋃ suc a$
395	394	fveq2d	$⊢ b = suc a \to g (⋃ b) = g (⋃ suc a)$
396	393 395	ifbieq2d	$⊢ b = suc a \to if (b = \emptyset, y, g (⋃ b)) = if (suc a = \emptyset, y, g (⋃ suc a))$
397		nsuceq0	$⊢ suc a \neq \emptyset$
398	397	neii	$⊢ \neg suc a = \emptyset$
399	398	iffalsei	$⊢ if (suc a = \emptyset, y, g (⋃ suc a)) = g (⋃ suc a)$
400	396 399	eqtrdi	$⊢ b = suc a \to if (b = \emptyset, y, g (⋃ b)) = g (⋃ suc a)$
401		fvex	$⊢ g (⋃ suc a) \in V$
402	400 296 401	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)$
403	392 402	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)$
404		nnord	$⊢ a \in ω \to Ord a$
405	376 404	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$
406		ordunisuc	$⊢ Ord a \to ⋃ suc a = a$
407	405 406	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$
408	407	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)$
409	403 408	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)$
410	379 389 409	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)$
411	410	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)$
412	263	sucex	$⊢ suc suc suc n \in V$
413	412	mptex	$⊢ (b \in suc suc suc n ⟼ if (b = \emptyset, y, g (⋃ b))) \in V$
414		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)$
415		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)$
416	415	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)$
417		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)$
418	417	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)$
419	416 418	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))$
420		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)$
421		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)$
422	420 421	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))$
423	422	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))$
424	414 419 423	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)))$
425	413 424	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))$
426	298 308 327 411 425	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))$
427	426	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))))$
428	427	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))))$
429	428	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)))$
430	429	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)))$
431	293 430	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))$
432		vex	$⊢ z \in V$
433	432	brresi	$⊢ y ({R ↾}_{A}) z \leftrightarrow (y \in A \land y R z)$
434	433	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))$
435	434	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))$
436	431 435	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)))$
437	214 436	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))))$
438	437	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)))$
439	438	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)))$
440	439	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)))$
441	175 202 440	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))$
442	441	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))$
443	442	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))))$
444	443	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))))$
445	27 68 82 96 164 444	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)))$
446	445	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))$
447	446	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