ttrcltr

Description: The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024)

		Ref	Expression
	Assertion	ttrcltr	$⊢ t++ R \circ t++ R \subseteq t++ R$

Proof

Step	Hyp	Ref	Expression
1		relco	$⊢ Rel (t++ R \circ t++ R)$
2		eldifi	$⊢ n \in (ω ∖ 1_{𝑜}) \to n \in ω$
3		eldifi	$⊢ m \in (ω ∖ 1_{𝑜}) \to m \in ω$
4		nnacl	$⊢ (n \in ω \land m \in ω) \to n +_{𝑜} m \in ω$
5	2 3 4	syl2an	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to n +_{𝑜} m \in ω$
6		eldif	$⊢ n \in (ω ∖ 1_{𝑜}) \leftrightarrow (n \in ω \land \neg n \in 1_{𝑜})$
7		1on	$⊢ 1_{𝑜} \in On$
8	7	onordi	$⊢ Ord 1_{𝑜}$
9		nnord	$⊢ n \in ω \to Ord n$
10		ordtri1	$⊢ (Ord 1_{𝑜} \land Ord n) \to (1_{𝑜} \subseteq n \leftrightarrow \neg n \in 1_{𝑜})$
11	8 9 10	sylancr	$⊢ n \in ω \to (1_{𝑜} \subseteq n \leftrightarrow \neg n \in 1_{𝑜})$
12	11	biimpar	$⊢ (n \in ω \land \neg n \in 1_{𝑜}) \to 1_{𝑜} \subseteq n$
13	6 12	sylbi	$⊢ n \in (ω ∖ 1_{𝑜}) \to 1_{𝑜} \subseteq n$
14	13	adantr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to 1_{𝑜} \subseteq n$
15		nnaword1	$⊢ (n \in ω \land m \in ω) \to n \subseteq n +_{𝑜} m$
16	2 3 15	syl2an	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to n \subseteq n +_{𝑜} m$
17	14 16	sstrd	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to 1_{𝑜} \subseteq n +_{𝑜} m$
18		nnord	$⊢ n +_{𝑜} m \in ω \to Ord (n +_{𝑜} m)$
19	5 18	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to Ord (n +_{𝑜} m)$
20		ordtri1	$⊢ (Ord 1_{𝑜} \land Ord (n +_{𝑜} m)) \to (1_{𝑜} \subseteq n +_{𝑜} m \leftrightarrow \neg n +_{𝑜} m \in 1_{𝑜})$
21	8 19 20	sylancr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (1_{𝑜} \subseteq n +_{𝑜} m \leftrightarrow \neg n +_{𝑜} m \in 1_{𝑜})$
22	17 21	mpbid	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to \neg n +_{𝑜} m \in 1_{𝑜}$
23	5 22	eldifd	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to n +_{𝑜} m \in (ω ∖ 1_{𝑜})$
24		0elsuc	$⊢ Ord (n +_{𝑜} m) \to \emptyset \in suc (n +_{𝑜} m)$
25	19 24	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to \emptyset \in suc (n +_{𝑜} m)$
26		eleq1	$⊢ p = \emptyset \to (p \in suc n \leftrightarrow \emptyset \in suc n)$
27		fveq2	$⊢ p = \emptyset \to f (p) = f (\emptyset)$
28		eqeq2	$⊢ p = \emptyset \to (n +_{𝑜} q = p \leftrightarrow n +_{𝑜} q = \emptyset)$
29	28	riotabidv	$⊢ p = \emptyset \to (ι q \in ω \| n +_{𝑜} q = p) = (ι q \in ω \| n +_{𝑜} q = \emptyset)$
30	29	fveq2d	$⊢ p = \emptyset \to g ((ι q \in ω \| n +_{𝑜} q = p)) = g ((ι q \in ω \| n +_{𝑜} q = \emptyset))$
31	26 27 30	ifbieq12d	$⊢ p = \emptyset \to if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p))) = if (\emptyset \in suc n, f (\emptyset), g ((ι q \in ω \| n +_{𝑜} q = \emptyset)))$
32		eqid	$⊢ (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p))))$
33		fvex	$⊢ f (\emptyset) \in V$
34		fvex	$⊢ g ((ι q \in ω \| n +_{𝑜} q = \emptyset)) \in V$
35	33 34	ifex	$⊢ if (\emptyset \in suc n, f (\emptyset), g ((ι q \in ω \| n +_{𝑜} q = \emptyset))) \in V$
36	31 32 35	fvmpt	$⊢ \emptyset \in suc (n +_{𝑜} m) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = if (\emptyset \in suc n, f (\emptyset), g ((ι q \in ω \| n +_{𝑜} q = \emptyset)))$
37	25 36	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = if (\emptyset \in suc n, f (\emptyset), g ((ι q \in ω \| n +_{𝑜} q = \emptyset)))$
38	2	adantr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to n \in ω$
39	38 9	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to Ord n$
40		0elsuc	$⊢ Ord n \to \emptyset \in suc n$
41	39 40	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to \emptyset \in suc n$
42	41	iftrued	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to if (\emptyset \in suc n, f (\emptyset), g ((ι q \in ω \| n +_{𝑜} q = \emptyset))) = f (\emptyset)$
43	37 42	eqtrd	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = f (\emptyset)$
44		simpl2l	$⊢ ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to f (\emptyset) = x$
45	43 44	sylan9eq	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = x$
46		ovex	$⊢ n +_{𝑜} m \in V$
47	46	sucid	$⊢ n +_{𝑜} m \in suc (n +_{𝑜} m)$
48		eleq1	$⊢ p = n +_{𝑜} m \to (p \in suc n \leftrightarrow n +_{𝑜} m \in suc n)$
49		fveq2	$⊢ p = n +_{𝑜} m \to f (p) = f (n +_{𝑜} m)$
50		eqeq2	$⊢ p = n +_{𝑜} m \to (n +_{𝑜} q = p \leftrightarrow n +_{𝑜} q = n +_{𝑜} m)$
51	50	riotabidv	$⊢ p = n +_{𝑜} m \to (ι q \in ω \| n +_{𝑜} q = p) = (ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m)$
52	51	fveq2d	$⊢ p = n +_{𝑜} m \to g ((ι q \in ω \| n +_{𝑜} q = p)) = g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m))$
53	48 49 52	ifbieq12d	$⊢ p = n +_{𝑜} m \to if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p))) = if (n +_{𝑜} m \in suc n, f (n +_{𝑜} m), g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m)))$
54		fvex	$⊢ f (n +_{𝑜} m) \in V$
55		fvex	$⊢ g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m)) \in V$
56	54 55	ifex	$⊢ if (n +_{𝑜} m \in suc n, f (n +_{𝑜} m), g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m))) \in V$
57	53 32 56	fvmpt	$⊢ n +_{𝑜} m \in suc (n +_{𝑜} m) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = if (n +_{𝑜} m \in suc n, f (n +_{𝑜} m), g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m)))$
58	47 57	mp1i	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = if (n +_{𝑜} m \in suc n, f (n +_{𝑜} m), g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m)))$
59		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
60	59	difeq2i	$⊢ ω ∖ 1_{𝑜} = ω ∖ suc \emptyset$
61	60	eleq2i	$⊢ n \in (ω ∖ 1_{𝑜}) \leftrightarrow n \in (ω ∖ suc \emptyset)$
62		peano1	$⊢ \emptyset \in ω$
63		eldifsucnn	$⊢ \emptyset \in ω \to (n \in (ω ∖ suc \emptyset) \leftrightarrow \exists x \in (ω ∖ \emptyset) n = suc x)$
64	62 63	ax-mp	$⊢ n \in (ω ∖ suc \emptyset) \leftrightarrow \exists x \in (ω ∖ \emptyset) n = suc x$
65		dif0	$⊢ ω ∖ \emptyset = ω$
66	65	rexeqi	$⊢ \exists x \in (ω ∖ \emptyset) n = suc x \leftrightarrow \exists x \in ω n = suc x$
67	61 64 66	3bitri	$⊢ n \in (ω ∖ 1_{𝑜}) \leftrightarrow \exists x \in ω n = suc x$
68	60	eleq2i	$⊢ m \in (ω ∖ 1_{𝑜}) \leftrightarrow m \in (ω ∖ suc \emptyset)$
69		eldifsucnn	$⊢ \emptyset \in ω \to (m \in (ω ∖ suc \emptyset) \leftrightarrow \exists y \in (ω ∖ \emptyset) m = suc y)$
70	62 69	ax-mp	$⊢ m \in (ω ∖ suc \emptyset) \leftrightarrow \exists y \in (ω ∖ \emptyset) m = suc y$
71	65	rexeqi	$⊢ \exists y \in (ω ∖ \emptyset) m = suc y \leftrightarrow \exists y \in ω m = suc y$
72	68 70 71	3bitri	$⊢ m \in (ω ∖ 1_{𝑜}) \leftrightarrow \exists y \in ω m = suc y$
73	67 72	anbi12i	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \leftrightarrow (\exists x \in ω n = suc x \land \exists y \in ω m = suc y)$
74		reeanv	$⊢ \exists x \in ω \exists y \in ω (n = suc x \land m = suc y) \leftrightarrow (\exists x \in ω n = suc x \land \exists y \in ω m = suc y)$
75	73 74	bitr4i	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \leftrightarrow \exists x \in ω \exists y \in ω (n = suc x \land m = suc y)$
76		peano2	$⊢ x \in ω \to suc x \in ω$
77		nnaword1	$⊢ (suc x \in ω \land y \in ω) \to suc x \subseteq suc x +_{𝑜} y$
78	76 77	sylan	$⊢ (x \in ω \land y \in ω) \to suc x \subseteq suc x +_{𝑜} y$
79	76	adantr	$⊢ (x \in ω \land y \in ω) \to suc x \in ω$
80		nnord	$⊢ suc x \in ω \to Ord suc x$
81	79 80	syl	$⊢ (x \in ω \land y \in ω) \to Ord suc x$
82		nnacl	$⊢ (suc x \in ω \land y \in ω) \to suc x +_{𝑜} y \in ω$
83	76 82	sylan	$⊢ (x \in ω \land y \in ω) \to suc x +_{𝑜} y \in ω$
84		nnord	$⊢ suc x +_{𝑜} y \in ω \to Ord (suc x +_{𝑜} y)$
85	83 84	syl	$⊢ (x \in ω \land y \in ω) \to Ord (suc x +_{𝑜} y)$
86		ordsucsssuc	$⊢ (Ord suc x \land Ord (suc x +_{𝑜} y)) \to (suc x \subseteq suc x +_{𝑜} y \leftrightarrow suc suc x \subseteq suc (suc x +_{𝑜} y))$
87	81 85 86	syl2anc	$⊢ (x \in ω \land y \in ω) \to (suc x \subseteq suc x +_{𝑜} y \leftrightarrow suc suc x \subseteq suc (suc x +_{𝑜} y))$
88	78 87	mpbid	$⊢ (x \in ω \land y \in ω) \to suc suc x \subseteq suc (suc x +_{𝑜} y)$
89		nnasuc	$⊢ (suc x \in ω \land y \in ω) \to suc x +_{𝑜} suc y = suc (suc x +_{𝑜} y)$
90	76 89	sylan	$⊢ (x \in ω \land y \in ω) \to suc x +_{𝑜} suc y = suc (suc x +_{𝑜} y)$
91	88 90	sseqtrrd	$⊢ (x \in ω \land y \in ω) \to suc suc x \subseteq suc x +_{𝑜} suc y$
92		peano2	$⊢ suc x \in ω \to suc suc x \in ω$
93	79 92	syl	$⊢ (x \in ω \land y \in ω) \to suc suc x \in ω$
94		nnord	$⊢ suc suc x \in ω \to Ord suc suc x$
95	93 94	syl	$⊢ (x \in ω \land y \in ω) \to Ord suc suc x$
96		peano2	$⊢ y \in ω \to suc y \in ω$
97		nnacl	$⊢ (suc x \in ω \land suc y \in ω) \to suc x +_{𝑜} suc y \in ω$
98	76 96 97	syl2an	$⊢ (x \in ω \land y \in ω) \to suc x +_{𝑜} suc y \in ω$
99		nnord	$⊢ suc x +_{𝑜} suc y \in ω \to Ord (suc x +_{𝑜} suc y)$
100	98 99	syl	$⊢ (x \in ω \land y \in ω) \to Ord (suc x +_{𝑜} suc y)$
101		ordtri1	$⊢ (Ord suc suc x \land Ord (suc x +_{𝑜} suc y)) \to (suc suc x \subseteq suc x +_{𝑜} suc y \leftrightarrow \neg suc x +_{𝑜} suc y \in suc suc x)$
102	95 100 101	syl2anc	$⊢ (x \in ω \land y \in ω) \to (suc suc x \subseteq suc x +_{𝑜} suc y \leftrightarrow \neg suc x +_{𝑜} suc y \in suc suc x)$
103	91 102	mpbid	$⊢ (x \in ω \land y \in ω) \to \neg suc x +_{𝑜} suc y \in suc suc x$
104		oveq12	$⊢ (n = suc x \land m = suc y) \to n +_{𝑜} m = suc x +_{𝑜} suc y$
105		suceq	$⊢ n = suc x \to suc n = suc suc x$
106	105	adantr	$⊢ (n = suc x \land m = suc y) \to suc n = suc suc x$
107	104 106	eleq12d	$⊢ (n = suc x \land m = suc y) \to (n +_{𝑜} m \in suc n \leftrightarrow suc x +_{𝑜} suc y \in suc suc x)$
108	107	notbid	$⊢ (n = suc x \land m = suc y) \to (\neg n +_{𝑜} m \in suc n \leftrightarrow \neg suc x +_{𝑜} suc y \in suc suc x)$
109	103 108	syl5ibrcom	$⊢ (x \in ω \land y \in ω) \to ((n = suc x \land m = suc y) \to \neg n +_{𝑜} m \in suc n)$
110	109	rexlimivv	$⊢ \exists x \in ω \exists y \in ω (n = suc x \land m = suc y) \to \neg n +_{𝑜} m \in suc n$
111	75 110	sylbi	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to \neg n +_{𝑜} m \in suc n$
112	111	iffalsed	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to if (n +_{𝑜} m \in suc n, f (n +_{𝑜} m), g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m))) = g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m))$
113	3	adantl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to m \in ω$
114	38	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land q \in ω) \to n \in ω$
115		simpr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land q \in ω) \to q \in ω$
116	113	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land q \in ω) \to m \in ω$
117		nnacan	$⊢ (n \in ω \land q \in ω \land m \in ω) \to (n +_{𝑜} q = n +_{𝑜} m \leftrightarrow q = m)$
118	114 115 116 117	syl3anc	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land q \in ω) \to (n +_{𝑜} q = n +_{𝑜} m \leftrightarrow q = m)$
119	113 118	riota5	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m) = m$
120	119	fveq2d	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to g ((ι q \in ω \| n +_{𝑜} q = n +_{𝑜} m)) = g (m)$
121	58 112 120	3eqtrd	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = g (m)$
122		simpr2r	$⊢ ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to g (m) = y$
123	121 122	sylan9eq	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = y$
124		simprl3	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to \forall a \in n f (a) R f (suc a)$
125		fveq2	$⊢ a = c \to f (a) = f (c)$
126		suceq	$⊢ a = c \to suc a = suc c$
127	126	fveq2d	$⊢ a = c \to f (suc a) = f (suc c)$
128	125 127	breq12d	$⊢ a = c \to (f (a) R f (suc a) \leftrightarrow f (c) R f (suc c))$
129	128	rspcv	$⊢ c \in n \to (\forall a \in n f (a) R f (suc a) \to f (c) R f (suc c))$
130	124 129	mpan9	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in n) \to f (c) R f (suc c)$
131		elelsuc	$⊢ c \in n \to c \in suc n$
132	131	adantl	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in n) \to c \in suc n$
133	132	iftrued	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in n) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) = f (c)$
134		ordsucelsuc	$⊢ Ord n \to (c \in n \leftrightarrow suc c \in suc n)$
135	39 134	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (c \in n \leftrightarrow suc c \in suc n)$
136	135	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to (c \in n \leftrightarrow suc c \in suc n)$
137	136	biimpa	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in n) \to suc c \in suc n$
138	137	iftrued	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in n) \to if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c))) = f (suc c)$
139	130 133 138	3brtr4d	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in n) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
140	139	adantlr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land c \in n) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
141	39	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to Ord n$
142	5	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to n +_{𝑜} m \in ω$
143		elnn	$⊢ (c \in (n +_{𝑜} m) \land n +_{𝑜} m \in ω) \to c \in ω$
144	143	ancoms	$⊢ (n +_{𝑜} m \in ω \land c \in (n +_{𝑜} m)) \to c \in ω$
145	142 144	sylan	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to c \in ω$
146		nnord	$⊢ c \in ω \to Ord c$
147	145 146	syl	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to Ord c$
148		ordtri3or	$⊢ (Ord n \land Ord c) \to (n \in c \lor n = c \lor c \in n)$
149	141 147 148	syl2an2r	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (n \in c \lor n = c \lor c \in n)$
150		3orel3	$⊢ \neg c \in n \to ((n \in c \lor n = c \lor c \in n) \to (n \in c \lor n = c))$
151	149 150	syl5com	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (\neg c \in n \to (n \in c \lor n = c))$
152		fveq2	$⊢ b = (ι q \in ω \| n +_{𝑜} q = c) \to g (b) = g ((ι q \in ω \| n +_{𝑜} q = c))$
153		suceq	$⊢ b = (ι q \in ω \| n +_{𝑜} q = c) \to suc b = suc (ι q \in ω \| n +_{𝑜} q = c)$
154	153	fveq2d	$⊢ b = (ι q \in ω \| n +_{𝑜} q = c) \to g (suc b) = g (suc (ι q \in ω \| n +_{𝑜} q = c))$
155	152 154	breq12d	$⊢ b = (ι q \in ω \| n +_{𝑜} q = c) \to (g (b) R g (suc b) \leftrightarrow g ((ι q \in ω \| n +_{𝑜} q = c)) R g (suc (ι q \in ω \| n +_{𝑜} q = c)))$
156		simprr3	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to \forall b \in m g (b) R g (suc b)$
157	156	adantr	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to \forall b \in m g (b) R g (suc b)$
158	157	adantr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \forall b \in m g (b) R g (suc b)$
159		ordelss	$⊢ (Ord c \land n \in c) \to n \subseteq c$
160	147 159	sylan	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to n \subseteq c$
161	38	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to n \in ω$
162	161	adantr	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to n \in ω$
163	145	adantr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to c \in ω$
164		nnawordex	$⊢ (n \in ω \land c \in ω) \to (n \subseteq c \leftrightarrow \exists q \in ω n +_{𝑜} q = c)$
165	162 163 164	syl2an2r	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (n \subseteq c \leftrightarrow \exists q \in ω n +_{𝑜} q = c)$
166	160 165	mpbid	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists q \in ω n +_{𝑜} q = c$
167		oveq2	$⊢ q = p \to n +_{𝑜} q = n +_{𝑜} p$
168	167	eqeq1d	$⊢ q = p \to (n +_{𝑜} q = c \leftrightarrow n +_{𝑜} p = c)$
169	168	cbvrexvw	$⊢ \exists q \in ω n +_{𝑜} q = c \leftrightarrow \exists p \in ω n +_{𝑜} p = c$
170	166 169	sylib	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists p \in ω n +_{𝑜} p = c$
171		simprr	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land (p \in ω \land n +_{𝑜} p = c)) \to n +_{𝑜} p = c$
172		simpllr	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land (p \in ω \land n +_{𝑜} p = c)) \to c \in (n +_{𝑜} m)$
173	171 172	eqeltrd	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land (p \in ω \land n +_{𝑜} p = c)) \to n +_{𝑜} p \in (n +_{𝑜} m)$
174		simprl	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land (p \in ω \land n +_{𝑜} p = c)) \to p \in ω$
175	3	ad4antlr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to m \in ω$
176	175	adantr	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land (p \in ω \land n +_{𝑜} p = c)) \to m \in ω$
177	162	adantr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to n \in ω$
178	177	adantr	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land (p \in ω \land n +_{𝑜} p = c)) \to n \in ω$
179		nnaord	$⊢ (p \in ω \land m \in ω \land n \in ω) \to (p \in m \leftrightarrow n +_{𝑜} p \in (n +_{𝑜} m))$
180	174 176 178 179	syl3anc	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land (p \in ω \land n +_{𝑜} p = c)) \to (p \in m \leftrightarrow n +_{𝑜} p \in (n +_{𝑜} m))$
181	173 180	mpbird	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land (p \in ω \land n +_{𝑜} p = c)) \to p \in m$
182	170 181 171	reximssdv	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists p \in m n +_{𝑜} p = c$
183		elnn	$⊢ (p \in m \land m \in ω) \to p \in ω$
184	183	ancoms	$⊢ (m \in ω \land p \in m) \to p \in ω$
185	175 184	sylan	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land p \in m) \to p \in ω$
186		nnasmo	$⊢ n \in ω \to \exists^{*} q \in ω n +_{𝑜} q = c$
187	177 186	syl	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists^{*} q \in ω n +_{𝑜} q = c$
188		reu5	$⊢ \exists! q \in ω n +_{𝑜} q = c \leftrightarrow (\exists q \in ω n +_{𝑜} q = c \land \exists^{*} q \in ω n +_{𝑜} q = c)$
189	166 187 188	sylanbrc	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists! q \in ω n +_{𝑜} q = c$
190	189	adantr	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land p \in m) \to \exists! q \in ω n +_{𝑜} q = c$
191	168	riota2	$⊢ (p \in ω \land \exists! q \in ω n +_{𝑜} q = c) \to (n +_{𝑜} p = c \leftrightarrow (ι q \in ω \| n +_{𝑜} q = c) = p)$
192	185 190 191	syl2anc	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land p \in m) \to (n +_{𝑜} p = c \leftrightarrow (ι q \in ω \| n +_{𝑜} q = c) = p)$
193		eqcom	$⊢ (ι q \in ω \| n +_{𝑜} q = c) = p \leftrightarrow p = (ι q \in ω \| n +_{𝑜} q = c)$
194	192 193	bitrdi	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land p \in m) \to (n +_{𝑜} p = c \leftrightarrow p = (ι q \in ω \| n +_{𝑜} q = c))$
195	194	rexbidva	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (\exists p \in m n +_{𝑜} p = c \leftrightarrow \exists p \in m p = (ι q \in ω \| n +_{𝑜} q = c))$
196	182 195	mpbid	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists p \in m p = (ι q \in ω \| n +_{𝑜} q = c)$
197		risset	$⊢ (ι q \in ω \| n +_{𝑜} q = c) \in m \leftrightarrow \exists p \in m p = (ι q \in ω \| n +_{𝑜} q = c)$
198	196 197	sylibr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (ι q \in ω \| n +_{𝑜} q = c) \in m$
199	155 158 198	rspcdva	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to g ((ι q \in ω \| n +_{𝑜} q = c)) R g (suc (ι q \in ω \| n +_{𝑜} q = c))$
200		simpr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to n \in c$
201		vex	$⊢ n \in V$
202	147	adantr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to Ord c$
203		ordelsuc	$⊢ (n \in V \land Ord c) \to (n \in c \leftrightarrow suc n \subseteq c)$
204	201 202 203	sylancr	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (n \in c \leftrightarrow suc n \subseteq c)$
205		peano2	$⊢ n \in ω \to suc n \in ω$
206	38 205	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to suc n \in ω$
207		nnord	$⊢ suc n \in ω \to Ord suc n$
208	206 207	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to Ord suc n$
209	208	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to Ord suc n$
210	209	adantr	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to Ord suc n$
211		ordtri1	$⊢ (Ord suc n \land Ord c) \to (suc n \subseteq c \leftrightarrow \neg c \in suc n)$
212	210 202 211	syl2an2r	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (suc n \subseteq c \leftrightarrow \neg c \in suc n)$
213	204 212	bitrd	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (n \in c \leftrightarrow \neg c \in suc n)$
214	200 213	mpbid	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \neg c \in suc n$
215	214	iffalsed	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) = g ((ι q \in ω \| n +_{𝑜} q = c))$
216		riotacl	$⊢ \exists! q \in ω n +_{𝑜} q = c \to (ι q \in ω \| n +_{𝑜} q = c) \in ω$
217	189 216	syl	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (ι q \in ω \| n +_{𝑜} q = c) \in ω$
218		nnasuc	$⊢ (n \in ω \land (ι q \in ω \| n +_{𝑜} q = c) \in ω) \to n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c) = suc (n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c))$
219	162 217 218	syl2an2r	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c) = suc (n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c))$
220		eqidd	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (ι q \in ω \| n +_{𝑜} q = c) = (ι q \in ω \| n +_{𝑜} q = c)$
221		nfriota1	$⊢ \underline{Ⅎ} q (ι q \in ω \| n +_{𝑜} q = c)$
222		nfcv	$⊢ \underline{Ⅎ} q n$
223		nfcv	$⊢ \underline{Ⅎ} q +_{𝑜}$
224	222 223 221	nfov	$⊢ \underline{Ⅎ} q (n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c))$
225	224	nfeq1	$⊢ Ⅎ q n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c) = c$
226		oveq2	$⊢ q = (ι q \in ω \| n +_{𝑜} q = c) \to n +_{𝑜} q = n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c)$
227	226	eqeq1d	$⊢ q = (ι q \in ω \| n +_{𝑜} q = c) \to (n +_{𝑜} q = c \leftrightarrow n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c) = c)$
228	221 225 227	riota2f	$⊢ ((ι q \in ω \| n +_{𝑜} q = c) \in ω \land \exists! q \in ω n +_{𝑜} q = c) \to (n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c) = c \leftrightarrow (ι q \in ω \| n +_{𝑜} q = c) = (ι q \in ω \| n +_{𝑜} q = c))$
229	217 189 228	syl2anc	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c) = c \leftrightarrow (ι q \in ω \| n +_{𝑜} q = c) = (ι q \in ω \| n +_{𝑜} q = c))$
230	220 229	mpbird	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c) = c$
231		suceq	$⊢ n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c) = c \to suc (n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c)) = suc c$
232	230 231	syl	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to suc (n +_{𝑜} (ι q \in ω \| n +_{𝑜} q = c)) = suc c$
233	219 232	eqtrd	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c) = suc c$
234		peano2	$⊢ (ι q \in ω \| n +_{𝑜} q = c) \in ω \to suc (ι q \in ω \| n +_{𝑜} q = c) \in ω$
235	217 234	syl	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to suc (ι q \in ω \| n +_{𝑜} q = c) \in ω$
236		peano2	$⊢ p \in ω \to suc p \in ω$
237		nnasuc	$⊢ (n \in ω \land p \in ω) \to n +_{𝑜} suc p = suc (n +_{𝑜} p)$
238	177 237	sylan	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land p \in ω) \to n +_{𝑜} suc p = suc (n +_{𝑜} p)$
239		oveq2	$⊢ q = suc p \to n +_{𝑜} q = n +_{𝑜} suc p$
240	239	eqeq1d	$⊢ q = suc p \to (n +_{𝑜} q = suc (n +_{𝑜} p) \leftrightarrow n +_{𝑜} suc p = suc (n +_{𝑜} p))$
241	240	rspcev	$⊢ (suc p \in ω \land n +_{𝑜} suc p = suc (n +_{𝑜} p)) \to \exists q \in ω n +_{𝑜} q = suc (n +_{𝑜} p)$
242	236 238 241	syl2an2	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land p \in ω) \to \exists q \in ω n +_{𝑜} q = suc (n +_{𝑜} p)$
243		suceq	$⊢ n +_{𝑜} p = c \to suc (n +_{𝑜} p) = suc c$
244	243	eqeq2d	$⊢ n +_{𝑜} p = c \to (n +_{𝑜} q = suc (n +_{𝑜} p) \leftrightarrow n +_{𝑜} q = suc c)$
245	244	rexbidv	$⊢ n +_{𝑜} p = c \to (\exists q \in ω n +_{𝑜} q = suc (n +_{𝑜} p) \leftrightarrow \exists q \in ω n +_{𝑜} q = suc c)$
246	242 245	syl5ibcom	$⊢ (((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \land p \in ω) \to (n +_{𝑜} p = c \to \exists q \in ω n +_{𝑜} q = suc c)$
247	246	rexlimdva	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (\exists p \in ω n +_{𝑜} p = c \to \exists q \in ω n +_{𝑜} q = suc c)$
248	170 247	mpd	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists q \in ω n +_{𝑜} q = suc c$
249		nnasmo	$⊢ n \in ω \to \exists^{*} q \in ω n +_{𝑜} q = suc c$
250	177 249	syl	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists^{*} q \in ω n +_{𝑜} q = suc c$
251		reu5	$⊢ \exists! q \in ω n +_{𝑜} q = suc c \leftrightarrow (\exists q \in ω n +_{𝑜} q = suc c \land \exists^{*} q \in ω n +_{𝑜} q = suc c)$
252	248 250 251	sylanbrc	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to \exists! q \in ω n +_{𝑜} q = suc c$
253	221	nfsuc	$⊢ \underline{Ⅎ} q suc (ι q \in ω \| n +_{𝑜} q = c)$
254	222 223 253	nfov	$⊢ \underline{Ⅎ} q (n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c))$
255	254	nfeq1	$⊢ Ⅎ q n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c) = suc c$
256		oveq2	$⊢ q = suc (ι q \in ω \| n +_{𝑜} q = c) \to n +_{𝑜} q = n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c)$
257	256	eqeq1d	$⊢ q = suc (ι q \in ω \| n +_{𝑜} q = c) \to (n +_{𝑜} q = suc c \leftrightarrow n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c) = suc c)$
258	253 255 257	riota2f	$⊢ (suc (ι q \in ω \| n +_{𝑜} q = c) \in ω \land \exists! q \in ω n +_{𝑜} q = suc c) \to (n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c) = suc c \leftrightarrow (ι q \in ω \| n +_{𝑜} q = suc c) = suc (ι q \in ω \| n +_{𝑜} q = c))$
259	235 252 258	syl2anc	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (n +_{𝑜} suc (ι q \in ω \| n +_{𝑜} q = c) = suc c \leftrightarrow (ι q \in ω \| n +_{𝑜} q = suc c) = suc (ι q \in ω \| n +_{𝑜} q = c))$
260	233 259	mpbid	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to (ι q \in ω \| n +_{𝑜} q = suc c) = suc (ι q \in ω \| n +_{𝑜} q = c)$
261	260	fveq2d	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to g ((ι q \in ω \| n +_{𝑜} q = suc c)) = g (suc (ι q \in ω \| n +_{𝑜} q = c))$
262	199 215 261	3brtr4d	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land n \in c) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R g ((ι q \in ω \| n +_{𝑜} q = suc c))$
263	262	ex	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (n \in c \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
264		fveq2	$⊢ b = \emptyset \to g (b) = g (\emptyset)$
265		suceq	$⊢ b = \emptyset \to suc b = suc \emptyset$
266	265 59	eqtr4di	$⊢ b = \emptyset \to suc b = 1_{𝑜}$
267	266	fveq2d	$⊢ b = \emptyset \to g (suc b) = g (1_{𝑜})$
268	264 267	breq12d	$⊢ b = \emptyset \to (g (b) R g (suc b) \leftrightarrow g (\emptyset) R g (1_{𝑜}))$
269		eldif	$⊢ m \in (ω ∖ 1_{𝑜}) \leftrightarrow (m \in ω \land \neg m \in 1_{𝑜})$
270		nnord	$⊢ m \in ω \to Ord m$
271		ordtri1	$⊢ (Ord 1_{𝑜} \land Ord m) \to (1_{𝑜} \subseteq m \leftrightarrow \neg m \in 1_{𝑜})$
272	8 270 271	sylancr	$⊢ m \in ω \to (1_{𝑜} \subseteq m \leftrightarrow \neg m \in 1_{𝑜})$
273	272	biimpar	$⊢ (m \in ω \land \neg m \in 1_{𝑜}) \to 1_{𝑜} \subseteq m$
274	269 273	sylbi	$⊢ m \in (ω ∖ 1_{𝑜}) \to 1_{𝑜} \subseteq m$
275	274	adantl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to 1_{𝑜} \subseteq m$
276	59 275	eqsstrrid	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to suc \emptyset \subseteq m$
277		0ex	$⊢ \emptyset \in V$
278	113 270	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to Ord m$
279		ordelsuc	$⊢ (\emptyset \in V \land Ord m) \to (\emptyset \in m \leftrightarrow suc \emptyset \subseteq m)$
280	277 278 279	sylancr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (\emptyset \in m \leftrightarrow suc \emptyset \subseteq m)$
281	276 280	mpbird	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to \emptyset \in m$
282	281	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to \emptyset \in m$
283	268 156 282	rspcdva	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to g (\emptyset) R g (1_{𝑜})$
284		simpl2r	$⊢ ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to f (n) = z$
285		simpr2l	$⊢ ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to g (\emptyset) = z$
286	284 285	eqtr4d	$⊢ ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to f (n) = g (\emptyset)$
287	286	adantl	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to f (n) = g (\emptyset)$
288		nnon	$⊢ n \in ω \to n \in On$
289	38 288	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to n \in On$
290		oa1suc	$⊢ n \in On \to n +_{𝑜} 1_{𝑜} = suc n$
291	289 290	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to n +_{𝑜} 1_{𝑜} = suc n$
292		1onn	$⊢ 1_{𝑜} \in ω$
293		oveq2	$⊢ q = 1_{𝑜} \to n +_{𝑜} q = n +_{𝑜} 1_{𝑜}$
294	293	eqeq1d	$⊢ q = 1_{𝑜} \to (n +_{𝑜} q = suc n \leftrightarrow n +_{𝑜} 1_{𝑜} = suc n)$
295	294	rspcev	$⊢ (1_{𝑜} \in ω \land n +_{𝑜} 1_{𝑜} = suc n) \to \exists q \in ω n +_{𝑜} q = suc n$
296	292 291 295	sylancr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to \exists q \in ω n +_{𝑜} q = suc n$
297		nnasmo	$⊢ n \in ω \to \exists^{*} q \in ω n +_{𝑜} q = suc n$
298	38 297	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to \exists^{*} q \in ω n +_{𝑜} q = suc n$
299		reu5	$⊢ \exists! q \in ω n +_{𝑜} q = suc n \leftrightarrow (\exists q \in ω n +_{𝑜} q = suc n \land \exists^{*} q \in ω n +_{𝑜} q = suc n)$
300	296 298 299	sylanbrc	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to \exists! q \in ω n +_{𝑜} q = suc n$
301	294	riota2	$⊢ (1_{𝑜} \in ω \land \exists! q \in ω n +_{𝑜} q = suc n) \to (n +_{𝑜} 1_{𝑜} = suc n \leftrightarrow (ι q \in ω \| n +_{𝑜} q = suc n) = 1_{𝑜})$
302	292 300 301	sylancr	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (n +_{𝑜} 1_{𝑜} = suc n \leftrightarrow (ι q \in ω \| n +_{𝑜} q = suc n) = 1_{𝑜})$
303	291 302	mpbid	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (ι q \in ω \| n +_{𝑜} q = suc n) = 1_{𝑜}$
304	303	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to (ι q \in ω \| n +_{𝑜} q = suc n) = 1_{𝑜}$
305	304	fveq2d	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to g ((ι q \in ω \| n +_{𝑜} q = suc n)) = g (1_{𝑜})$
306	283 287 305	3brtr4d	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to f (n) R g ((ι q \in ω \| n +_{𝑜} q = suc n))$
307	201	sucid	$⊢ n \in suc n$
308	307	iftruei	$⊢ if (n \in suc n, f (n), g ((ι q \in ω \| n +_{𝑜} q = c))) = f (n)$
309		eleq1	$⊢ n = c \to (n \in suc n \leftrightarrow c \in suc n)$
310		fveq2	$⊢ n = c \to f (n) = f (c)$
311	309 310	ifbieq1d	$⊢ n = c \to if (n \in suc n, f (n), g ((ι q \in ω \| n +_{𝑜} q = c))) = if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c)))$
312	308 311	eqtr3id	$⊢ n = c \to f (n) = if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c)))$
313		suceq	$⊢ n = c \to suc n = suc c$
314	313	eqeq2d	$⊢ n = c \to (n +_{𝑜} q = suc n \leftrightarrow n +_{𝑜} q = suc c)$
315	314	riotabidv	$⊢ n = c \to (ι q \in ω \| n +_{𝑜} q = suc n) = (ι q \in ω \| n +_{𝑜} q = suc c)$
316	315	fveq2d	$⊢ n = c \to g ((ι q \in ω \| n +_{𝑜} q = suc n)) = g ((ι q \in ω \| n +_{𝑜} q = suc c))$
317	312 316	breq12d	$⊢ n = c \to (f (n) R g ((ι q \in ω \| n +_{𝑜} q = suc n)) \leftrightarrow if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
318	306 317	syl5ibcom	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to (n = c \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
319	318	adantr	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (n = c \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
320	263 319	jaod	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to ((n \in c \lor n = c) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
321	151 320	syld	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (\neg c \in n \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
322	321	imp	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land \neg c \in n) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R g ((ι q \in ω \| n +_{𝑜} q = suc c))$
323	135	notbid	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (\neg c \in n \leftrightarrow \neg suc c \in suc n)$
324	323	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to (\neg c \in n \leftrightarrow \neg suc c \in suc n)$
325	324	adantr	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (\neg c \in n \leftrightarrow \neg suc c \in suc n)$
326	325	biimpa	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land \neg c \in n) \to \neg suc c \in suc n$
327	326	iffalsed	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land \neg c \in n) \to if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c))) = g ((ι q \in ω \| n +_{𝑜} q = suc c))$
328	322 327	breqtrrd	$⊢ ((((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \land \neg c \in n) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
329	140 328	pm2.61dan	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) R if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
330		elelsuc	$⊢ c \in (n +_{𝑜} m) \to c \in suc (n +_{𝑜} m)$
331	330	adantl	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to c \in suc (n +_{𝑜} m)$
332		eleq1	$⊢ p = c \to (p \in suc n \leftrightarrow c \in suc n)$
333		fveq2	$⊢ p = c \to f (p) = f (c)$
334		eqeq2	$⊢ p = c \to (n +_{𝑜} q = p \leftrightarrow n +_{𝑜} q = c)$
335	334	riotabidv	$⊢ p = c \to (ι q \in ω \| n +_{𝑜} q = p) = (ι q \in ω \| n +_{𝑜} q = c)$
336	335	fveq2d	$⊢ p = c \to g ((ι q \in ω \| n +_{𝑜} q = p)) = g ((ι q \in ω \| n +_{𝑜} q = c))$
337	332 333 336	ifbieq12d	$⊢ p = c \to if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p))) = if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c)))$
338		fvex	$⊢ f (c) \in V$
339		fvex	$⊢ g ((ι q \in ω \| n +_{𝑜} q = c)) \in V$
340	338 339	ifex	$⊢ if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c))) \in V$
341	337 32 340	fvmpt	$⊢ c \in suc (n +_{𝑜} m) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) = if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c)))$
342	331 341	syl	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) = if (c \in suc n, f (c), g ((ι q \in ω \| n +_{𝑜} q = c)))$
343		ordsucelsuc	$⊢ Ord (n +_{𝑜} m) \to (c \in (n +_{𝑜} m) \leftrightarrow suc c \in suc (n +_{𝑜} m))$
344	19 343	syl	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (c \in (n +_{𝑜} m) \leftrightarrow suc c \in suc (n +_{𝑜} m))$
345	344	adantr	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to (c \in (n +_{𝑜} m) \leftrightarrow suc c \in suc (n +_{𝑜} m))$
346	345	biimpa	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to suc c \in suc (n +_{𝑜} m)$
347		eleq1	$⊢ p = suc c \to (p \in suc n \leftrightarrow suc c \in suc n)$
348		fveq2	$⊢ p = suc c \to f (p) = f (suc c)$
349		eqeq2	$⊢ p = suc c \to (n +_{𝑜} q = p \leftrightarrow n +_{𝑜} q = suc c)$
350	349	riotabidv	$⊢ p = suc c \to (ι q \in ω \| n +_{𝑜} q = p) = (ι q \in ω \| n +_{𝑜} q = suc c)$
351	350	fveq2d	$⊢ p = suc c \to g ((ι q \in ω \| n +_{𝑜} q = p)) = g ((ι q \in ω \| n +_{𝑜} q = suc c))$
352	347 348 351	ifbieq12d	$⊢ p = suc c \to if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p))) = if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
353		fvex	$⊢ f (suc c) \in V$
354		fvex	$⊢ g ((ι q \in ω \| n +_{𝑜} q = suc c)) \in V$
355	353 354	ifex	$⊢ if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c))) \in V$
356	352 32 355	fvmpt	$⊢ suc c \in suc (n +_{𝑜} m) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c) = if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
357	346 356	syl	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c) = if (suc c \in suc n, f (suc c), g ((ι q \in ω \| n +_{𝑜} q = suc c)))$
358	329 342 357	3brtr4d	$⊢ (((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \land c \in (n +_{𝑜} m)) \to (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) R (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c)$
359	358	ralrimiva	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to \forall c \in (n +_{𝑜} m) (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) R (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c)$
360		fvex	$⊢ f (p) \in V$
361		fvex	$⊢ g ((ι q \in ω \| n +_{𝑜} q = p)) \in V$
362	360 361	ifex	$⊢ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p))) \in V$
363	362 32	fnmpti	$⊢ (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) Fn suc (n +_{𝑜} m)$
364	46	sucex	$⊢ suc (n +_{𝑜} m) \in V$
365	364	mptex	$⊢ (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \in V$
366		fneq1	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to (h Fn suc (n +_{𝑜} m) \leftrightarrow (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) Fn suc (n +_{𝑜} m))$
367		fveq1	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to h (\emptyset) = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset)$
368	367	eqeq1d	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to (h (\emptyset) = x \leftrightarrow (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = x)$
369		fveq1	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to h (n +_{𝑜} m) = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m)$
370	369	eqeq1d	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to (h (n +_{𝑜} m) = y \leftrightarrow (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = y)$
371	368 370	anbi12d	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to ((h (\emptyset) = x \land h (n +_{𝑜} m) = y) \leftrightarrow ((p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = x \land (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = y))$
372		fveq1	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to h (c) = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c)$
373		fveq1	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to h (suc c) = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c)$
374	372 373	breq12d	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to (h (c) R h (suc c) \leftrightarrow (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) R (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c))$
375	374	ralbidv	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to (\forall c \in (n +_{𝑜} m) h (c) R h (suc c) \leftrightarrow \forall c \in (n +_{𝑜} m) (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) R (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c))$
376	366 371 375	3anbi123d	$⊢ h = (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) \to ((h Fn suc (n +_{𝑜} m) \land (h (\emptyset) = x \land h (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) h (c) R h (suc c)) \leftrightarrow ((p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) Fn suc (n +_{𝑜} m) \land ((p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = x \land (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) R (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c)))$
377	365 376	spcev	$⊢ ((p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) Fn suc (n +_{𝑜} m) \land ((p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = x \land (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) R (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c)) \to \exists h (h Fn suc (n +_{𝑜} m) \land (h (\emptyset) = x \land h (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) h (c) R h (suc c))$
378	363 377	mp3an1	$⊢ (((p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (\emptyset) = x \land (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (c) R (p \in suc (n +_{𝑜} m) ⟼ if (p \in suc n, f (p), g ((ι q \in ω \| n +_{𝑜} q = p)))) (suc c)) \to \exists h (h Fn suc (n +_{𝑜} m) \land (h (\emptyset) = x \land h (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) h (c) R h (suc c))$
379	45 123 359 378	syl21anc	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to \exists h (h Fn suc (n +_{𝑜} m) \land (h (\emptyset) = x \land h (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) h (c) R h (suc c))$
380		suceq	$⊢ p = n +_{𝑜} m \to suc p = suc (n +_{𝑜} m)$
381	380	fneq2d	$⊢ p = n +_{𝑜} m \to (h Fn suc p \leftrightarrow h Fn suc (n +_{𝑜} m))$
382		fveqeq2	$⊢ p = n +_{𝑜} m \to (h (p) = y \leftrightarrow h (n +_{𝑜} m) = y)$
383	382	anbi2d	$⊢ p = n +_{𝑜} m \to ((h (\emptyset) = x \land h (p) = y) \leftrightarrow (h (\emptyset) = x \land h (n +_{𝑜} m) = y))$
384		raleq	$⊢ p = n +_{𝑜} m \to (\forall c \in p h (c) R h (suc c) \leftrightarrow \forall c \in (n +_{𝑜} m) h (c) R h (suc c))$
385	381 383 384	3anbi123d	$⊢ p = n +_{𝑜} m \to ((h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c)) \leftrightarrow (h Fn suc (n +_{𝑜} m) \land (h (\emptyset) = x \land h (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) h (c) R h (suc c)))$
386	385	exbidv	$⊢ p = n +_{𝑜} m \to (\exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c)) \leftrightarrow \exists h (h Fn suc (n +_{𝑜} m) \land (h (\emptyset) = x \land h (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) h (c) R h (suc c)))$
387	386	rspcev	$⊢ (n +_{𝑜} m \in (ω ∖ 1_{𝑜}) \land \exists h (h Fn suc (n +_{𝑜} m) \land (h (\emptyset) = x \land h (n +_{𝑜} m) = y) \land \forall c \in (n +_{𝑜} m) h (c) R h (suc c))) \to \exists p \in (ω ∖ 1_{𝑜}) \exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c))$
388	23 379 387	syl2an2r	$⊢ ((n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \land ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))) \to \exists p \in (ω ∖ 1_{𝑜}) \exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c))$
389	388	ex	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to \exists p \in (ω ∖ 1_{𝑜}) \exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c)))$
390	389	exlimdvv	$⊢ (n \in (ω ∖ 1_{𝑜}) \land m \in (ω ∖ 1_{𝑜})) \to (\exists f \exists g ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to \exists p \in (ω ∖ 1_{𝑜}) \exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c)))$
391	390	rexlimivv	$⊢ \exists n \in (ω ∖ 1_{𝑜}) \exists m \in (ω ∖ 1_{𝑜}) \exists f \exists g ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to \exists p \in (ω ∖ 1_{𝑜}) \exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c))$
392	391	exlimiv	$⊢ \exists z \exists n \in (ω ∖ 1_{𝑜}) \exists m \in (ω ∖ 1_{𝑜}) \exists f \exists g ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \to \exists p \in (ω ∖ 1_{𝑜}) \exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c))$
393		vex	$⊢ x \in V$
394		vex	$⊢ y \in V$
395	393 394	opelco	$⊢ ⟨x, y⟩ \in (t++ R \circ t++ R) \leftrightarrow \exists z (x t++ R z \land z t++ R y)$
396		reeanv	$⊢ \exists n \in (ω ∖ 1_{𝑜}) \exists m \in (ω ∖ 1_{𝑜}) (\exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land \exists g (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \leftrightarrow (\exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land \exists m \in (ω ∖ 1_{𝑜}) \exists g (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))$
397		eeanv	$⊢ \exists f \exists g ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \leftrightarrow (\exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land \exists g (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))$
398	397	2rexbii	$⊢ \exists n \in (ω ∖ 1_{𝑜}) \exists m \in (ω ∖ 1_{𝑜}) \exists f \exists g ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))) \leftrightarrow \exists n \in (ω ∖ 1_{𝑜}) \exists m \in (ω ∖ 1_{𝑜}) (\exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land \exists g (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))$
399		brttrcl	$⊢ x t++ R z \leftrightarrow \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a))$
400		brttrcl	$⊢ z t++ R y \leftrightarrow \exists m \in (ω ∖ 1_{𝑜}) \exists g (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b))$
401	399 400	anbi12i	$⊢ (x t++ R z \land z t++ R y) \leftrightarrow (\exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land \exists m \in (ω ∖ 1_{𝑜}) \exists g (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))$
402	396 398 401	3bitr4ri	$⊢ (x t++ R z \land z t++ R y) \leftrightarrow \exists n \in (ω ∖ 1_{𝑜}) \exists m \in (ω ∖ 1_{𝑜}) \exists f \exists g ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))$
403	402	exbii	$⊢ \exists z (x t++ R z \land z t++ R y) \leftrightarrow \exists z \exists n \in (ω ∖ 1_{𝑜}) \exists m \in (ω ∖ 1_{𝑜}) \exists f \exists g ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))$
404	395 403	bitri	$⊢ ⟨x, y⟩ \in (t++ R \circ t++ R) \leftrightarrow \exists z \exists n \in (ω ∖ 1_{𝑜}) \exists m \in (ω ∖ 1_{𝑜}) \exists f \exists g ((f Fn suc n \land (f (\emptyset) = x \land f (n) = z) \land \forall a \in n f (a) R f (suc a)) \land (g Fn suc m \land (g (\emptyset) = z \land g (m) = y) \land \forall b \in m g (b) R g (suc b)))$
405		df-br	$⊢ x t++ R y \leftrightarrow ⟨x, y⟩ \in t++ R$
406		brttrcl	$⊢ x t++ R y \leftrightarrow \exists p \in (ω ∖ 1_{𝑜}) \exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c))$
407	405 406	bitr3i	$⊢ ⟨x, y⟩ \in t++ R \leftrightarrow \exists p \in (ω ∖ 1_{𝑜}) \exists h (h Fn suc p \land (h (\emptyset) = x \land h (p) = y) \land \forall c \in p h (c) R h (suc c))$
408	392 404 407	3imtr4i	$⊢ ⟨x, y⟩ \in (t++ R \circ t++ R) \to ⟨x, y⟩ \in t++ R$
409	1 408	relssi	$⊢ t++ R \circ t++ R \subseteq t++ R$

Metamath Proof Explorer

Theorem ttrcltr

Proof