ttrclss

Description: If R is a subclass of S and S is transitive, then the transitive closure of R is a subclass of S . (Contributed by Scott Fenton, 20-Oct-2024)

		Ref	Expression
	Assertion	ttrclss	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to t++ R \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		suceq	$⊢ m = \emptyset \to suc m = suc \emptyset$
2	1	suceqd	$⊢ m = \emptyset \to suc suc m = suc suc \emptyset$
3	2	fneq2d	$⊢ m = \emptyset \to (f Fn suc suc m \leftrightarrow f Fn suc suc \emptyset)$
4		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
5	1 4	eqtr4di	$⊢ m = \emptyset \to suc m = 1_{𝑜}$
6	5	fveqeq2d	$⊢ m = \emptyset \to (f (suc m) = y \leftrightarrow f (1_{𝑜}) = y)$
7	6	anbi2d	$⊢ m = \emptyset \to ((f (\emptyset) = x \land f (suc m) = y) \leftrightarrow (f (\emptyset) = x \land f (1_{𝑜}) = y))$
8		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
9	5 8	eqtrdi	$⊢ m = \emptyset \to suc m = \{\emptyset\}$
10	9	raleqdv	$⊢ m = \emptyset \to (\forall a \in suc m f (a) R f (suc a) \leftrightarrow \forall a \in \{\emptyset\} f (a) R f (suc a))$
11		0ex	$⊢ \emptyset \in V$
12		fveq2	$⊢ a = \emptyset \to f (a) = f (\emptyset)$
13		suceq	$⊢ a = \emptyset \to suc a = suc \emptyset$
14	13 4	eqtr4di	$⊢ a = \emptyset \to suc a = 1_{𝑜}$
15	14	fveq2d	$⊢ a = \emptyset \to f (suc a) = f (1_{𝑜})$
16	12 15	breq12d	$⊢ a = \emptyset \to (f (a) R f (suc a) \leftrightarrow f (\emptyset) R f (1_{𝑜}))$
17	11 16	ralsn	$⊢ \forall a \in \{\emptyset\} f (a) R f (suc a) \leftrightarrow f (\emptyset) R f (1_{𝑜})$
18	10 17	bitrdi	$⊢ m = \emptyset \to (\forall a \in suc m f (a) R f (suc a) \leftrightarrow f (\emptyset) R f (1_{𝑜}))$
19	3 7 18	3anbi123d	$⊢ m = \emptyset \to ((f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})))$
20	19	exbidv	$⊢ m = \emptyset \to (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow \exists f (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})))$
21	20	imbi1d	$⊢ m = \emptyset \to ((\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow (\exists f (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x S y))$
22	21	albidv	$⊢ m = \emptyset \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow \forall y (\exists f (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x S y))$
23	22	imbi2d	$⊢ m = \emptyset \to (((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y)) \leftrightarrow ((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x S y)))$
24		suceq	$⊢ m = i \to suc m = suc i$
25	24	suceqd	$⊢ m = i \to suc suc m = suc suc i$
26	25	fneq2d	$⊢ m = i \to (f Fn suc suc m \leftrightarrow f Fn suc suc i)$
27	24	fveqeq2d	$⊢ m = i \to (f (suc m) = y \leftrightarrow f (suc i) = y)$
28	27	anbi2d	$⊢ m = i \to ((f (\emptyset) = x \land f (suc m) = y) \leftrightarrow (f (\emptyset) = x \land f (suc i) = y))$
29	24	raleqdv	$⊢ m = i \to (\forall a \in suc m f (a) R f (suc a) \leftrightarrow \forall a \in suc i f (a) R f (suc a))$
30		fveq2	$⊢ a = b \to f (a) = f (b)$
31		suceq	$⊢ a = b \to suc a = suc b$
32	31	fveq2d	$⊢ a = b \to f (suc a) = f (suc b)$
33	30 32	breq12d	$⊢ a = b \to (f (a) R f (suc a) \leftrightarrow f (b) R f (suc b))$
34	33	cbvralvw	$⊢ \forall a \in suc i f (a) R f (suc a) \leftrightarrow \forall b \in suc i f (b) R f (suc b)$
35	29 34	bitrdi	$⊢ m = i \to (\forall a \in suc m f (a) R f (suc a) \leftrightarrow \forall b \in suc i f (b) R f (suc b))$
36	26 28 35	3anbi123d	$⊢ m = i \to ((f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow (f Fn suc suc i \land (f (\emptyset) = x \land f (suc i) = y) \land \forall b \in suc i f (b) R f (suc b)))$
37	36	exbidv	$⊢ m = i \to (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow \exists f (f Fn suc suc i \land (f (\emptyset) = x \land f (suc i) = y) \land \forall b \in suc i f (b) R f (suc b)))$
38		fneq1	$⊢ f = g \to (f Fn suc suc i \leftrightarrow g Fn suc suc i)$
39		fveq1	$⊢ f = g \to f (\emptyset) = g (\emptyset)$
40	39	eqeq1d	$⊢ f = g \to (f (\emptyset) = x \leftrightarrow g (\emptyset) = x)$
41		fveq1	$⊢ f = g \to f (suc i) = g (suc i)$
42	41	eqeq1d	$⊢ f = g \to (f (suc i) = y \leftrightarrow g (suc i) = y)$
43	40 42	anbi12d	$⊢ f = g \to ((f (\emptyset) = x \land f (suc i) = y) \leftrightarrow (g (\emptyset) = x \land g (suc i) = y))$
44		fveq1	$⊢ f = g \to f (b) = g (b)$
45		fveq1	$⊢ f = g \to f (suc b) = g (suc b)$
46	44 45	breq12d	$⊢ f = g \to (f (b) R f (suc b) \leftrightarrow g (b) R g (suc b))$
47	46	ralbidv	$⊢ f = g \to (\forall b \in suc i f (b) R f (suc b) \leftrightarrow \forall b \in suc i g (b) R g (suc b))$
48	38 43 47	3anbi123d	$⊢ f = g \to ((f Fn suc suc i \land (f (\emptyset) = x \land f (suc i) = y) \land \forall b \in suc i f (b) R f (suc b)) \leftrightarrow (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b)))$
49	48	cbvexvw	$⊢ \exists f (f Fn suc suc i \land (f (\emptyset) = x \land f (suc i) = y) \land \forall b \in suc i f (b) R f (suc b)) \leftrightarrow \exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b))$
50	37 49	bitrdi	$⊢ m = i \to (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow \exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b)))$
51	50	imbi1d	$⊢ m = i \to ((\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b)) \to x S y))$
52	51	albidv	$⊢ m = i \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow \forall y (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b)) \to x S y))$
53		eqeq2	$⊢ y = z \to (g (suc i) = y \leftrightarrow g (suc i) = z)$
54	53	anbi2d	$⊢ y = z \to ((g (\emptyset) = x \land g (suc i) = y) \leftrightarrow (g (\emptyset) = x \land g (suc i) = z))$
55	54	3anbi2d	$⊢ y = z \to ((g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b)) \leftrightarrow (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)))$
56	55	exbidv	$⊢ y = z \to (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b)) \leftrightarrow \exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)))$
57		breq2	$⊢ y = z \to (x S y \leftrightarrow x S z)$
58	56 57	imbi12d	$⊢ y = z \to ((\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b)) \to x S y) \leftrightarrow (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z))$
59	58	cbvalvw	$⊢ \forall y (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = y) \land \forall b \in suc i g (b) R g (suc b)) \to x S y) \leftrightarrow \forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z)$
60	52 59	bitrdi	$⊢ m = i \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow \forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z))$
61	60	imbi2d	$⊢ m = i \to (((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y)) \leftrightarrow ((R \subseteq S \land S \circ S \subseteq S) \to \forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z)))$
62		suceq	$⊢ m = suc i \to suc m = suc suc i$
63	62	suceqd	$⊢ m = suc i \to suc suc m = suc suc suc i$
64	63	fneq2d	$⊢ m = suc i \to (f Fn suc suc m \leftrightarrow f Fn suc suc suc i)$
65	62	fveqeq2d	$⊢ m = suc i \to (f (suc m) = y \leftrightarrow f (suc suc i) = y)$
66	65	anbi2d	$⊢ m = suc i \to ((f (\emptyset) = x \land f (suc m) = y) \leftrightarrow (f (\emptyset) = x \land f (suc suc i) = y))$
67	62	raleqdv	$⊢ m = suc i \to (\forall a \in suc m f (a) R f (suc a) \leftrightarrow \forall a \in suc suc i f (a) R f (suc a))$
68	64 66 67	3anbi123d	$⊢ m = suc i \to ((f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)))$
69	68	exbidv	$⊢ m = suc i \to (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow \exists f (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)))$
70	69	imbi1d	$⊢ m = suc i \to ((\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow (\exists f (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y))$
71	70	albidv	$⊢ m = suc i \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow \forall y (\exists f (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y))$
72	71	imbi2d	$⊢ m = suc i \to (((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y)) \leftrightarrow ((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y)))$
73		suceq	$⊢ m = n \to suc m = suc n$
74	73	suceqd	$⊢ m = n \to suc suc m = suc suc n$
75	74	fneq2d	$⊢ m = n \to (f Fn suc suc m \leftrightarrow f Fn suc suc n)$
76	73	fveqeq2d	$⊢ m = n \to (f (suc m) = y \leftrightarrow f (suc n) = y)$
77	76	anbi2d	$⊢ m = n \to ((f (\emptyset) = x \land f (suc m) = y) \leftrightarrow (f (\emptyset) = x \land f (suc n) = y))$
78	73	raleqdv	$⊢ m = n \to (\forall a \in suc m f (a) R f (suc a) \leftrightarrow \forall a \in suc n f (a) R f (suc a))$
79	75 77 78	3anbi123d	$⊢ m = n \to ((f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)))$
80	79	exbidv	$⊢ m = n \to (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \leftrightarrow \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)))$
81	80	imbi1d	$⊢ m = n \to ((\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y))$
82	81	albidv	$⊢ m = n \to (\forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y) \leftrightarrow \forall y (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y))$
83	82	imbi2d	$⊢ m = n \to (((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc m \land (f (\emptyset) = x \land f (suc m) = y) \land \forall a \in suc m f (a) R f (suc a)) \to x S y)) \leftrightarrow ((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y)))$
84		breq12	$⊢ (f (\emptyset) = x \land f (1_{𝑜}) = y) \to (f (\emptyset) R f (1_{𝑜}) \leftrightarrow x R y)$
85	84	biimpa	$⊢ ((f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x R y$
86	85	3adant1	$⊢ (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x R y$
87		ssbr	$⊢ R \subseteq S \to (x R y \to x S y)$
88	87	adantr	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to (x R y \to x S y)$
89	86 88	syl5	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to ((f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x S y)$
90	89	exlimdv	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to (\exists f (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x S y)$
91	90	alrimiv	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x S y)$
92		fvex	$⊢ f (suc i) \in V$
93		eqeq2	$⊢ z = f (suc i) \to (g (suc i) = z \leftrightarrow g (suc i) = f (suc i))$
94	93	anbi2d	$⊢ z = f (suc i) \to ((g (\emptyset) = x \land g (suc i) = z) \leftrightarrow (g (\emptyset) = x \land g (suc i) = f (suc i)))$
95	94	3anbi2d	$⊢ z = f (suc i) \to ((g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \leftrightarrow (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b)))$
96	95	exbidv	$⊢ z = f (suc i) \to (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \leftrightarrow \exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b)))$
97		breq2	$⊢ z = f (suc i) \to (x S z \leftrightarrow x S f (suc i))$
98	96 97	imbi12d	$⊢ z = f (suc i) \to ((\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z) \leftrightarrow (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b)) \to x S f (suc i)))$
99	92 98	spcv	$⊢ \forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z) \to (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b)) \to x S f (suc i))$
100		simpr1	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to f Fn suc suc suc i$
101		sssucid	$⊢ suc suc i \subseteq suc suc suc i$
102		fnssres	$⊢ (f Fn suc suc suc i \land suc suc i \subseteq suc suc suc i) \to ({f ↾}_{suc suc i}) Fn suc suc i$
103	100 101 102	sylancl	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to ({f ↾}_{suc suc i}) Fn suc suc i$
104		peano2	$⊢ i \in ω \to suc i \in ω$
105	104	ad2antrr	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to suc i \in ω$
106		nnord	$⊢ suc i \in ω \to Ord suc i$
107		0elsuc	$⊢ Ord suc i \to \emptyset \in suc suc i$
108	105 106 107	3syl	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to \emptyset \in suc suc i$
109	108	fvresd	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to ({f ↾}_{suc suc i}) (\emptyset) = f (\emptyset)$
110		simpr2l	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to f (\emptyset) = x$
111	109 110	eqtrd	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to ({f ↾}_{suc suc i}) (\emptyset) = x$
112		vex	$⊢ i \in V$
113	112	sucex	$⊢ suc i \in V$
114	113	sucid	$⊢ suc i \in suc suc i$
115		fvres	$⊢ suc i \in suc suc i \to ({f ↾}_{suc suc i}) (suc i) = f (suc i)$
116	114 115	mp1i	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to ({f ↾}_{suc suc i}) (suc i) = f (suc i)$
117		simplr3	$⊢ (((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \land b \in suc i) \to \forall a \in suc suc i f (a) R f (suc a)$
118		elelsuc	$⊢ b \in suc i \to b \in suc suc i$
119	118	adantl	$⊢ (((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \land b \in suc i) \to b \in suc suc i$
120	33 117 119	rspcdva	$⊢ (((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \land b \in suc i) \to f (b) R f (suc b)$
121	119	fvresd	$⊢ (((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \land b \in suc i) \to ({f ↾}_{suc suc i}) (b) = f (b)$
122		ordsucelsuc	$⊢ Ord suc i \to (b \in suc i \leftrightarrow suc b \in suc suc i)$
123	105 106 122	3syl	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to (b \in suc i \leftrightarrow suc b \in suc suc i)$
124	123	biimpa	$⊢ (((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \land b \in suc i) \to suc b \in suc suc i$
125	124	fvresd	$⊢ (((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \land b \in suc i) \to ({f ↾}_{suc suc i}) (suc b) = f (suc b)$
126	120 121 125	3brtr4d	$⊢ (((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \land b \in suc i) \to ({f ↾}_{suc suc i}) (b) R ({f ↾}_{suc suc i}) (suc b)$
127	126	ralrimiva	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to \forall b \in suc i ({f ↾}_{suc suc i}) (b) R ({f ↾}_{suc suc i}) (suc b)$
128		vex	$⊢ f \in V$
129	128	resex	$⊢ {f ↾}_{suc suc i} \in V$
130		fneq1	$⊢ g = {f ↾}_{suc suc i} \to (g Fn suc suc i \leftrightarrow ({f ↾}_{suc suc i}) Fn suc suc i)$
131		fveq1	$⊢ g = {f ↾}_{suc suc i} \to g (\emptyset) = ({f ↾}_{suc suc i}) (\emptyset)$
132	131	eqeq1d	$⊢ g = {f ↾}_{suc suc i} \to (g (\emptyset) = x \leftrightarrow ({f ↾}_{suc suc i}) (\emptyset) = x)$
133		fveq1	$⊢ g = {f ↾}_{suc suc i} \to g (suc i) = ({f ↾}_{suc suc i}) (suc i)$
134	133	eqeq1d	$⊢ g = {f ↾}_{suc suc i} \to (g (suc i) = f (suc i) \leftrightarrow ({f ↾}_{suc suc i}) (suc i) = f (suc i))$
135	132 134	anbi12d	$⊢ g = {f ↾}_{suc suc i} \to ((g (\emptyset) = x \land g (suc i) = f (suc i)) \leftrightarrow (({f ↾}_{suc suc i}) (\emptyset) = x \land ({f ↾}_{suc suc i}) (suc i) = f (suc i)))$
136		fveq1	$⊢ g = {f ↾}_{suc suc i} \to g (b) = ({f ↾}_{suc suc i}) (b)$
137		fveq1	$⊢ g = {f ↾}_{suc suc i} \to g (suc b) = ({f ↾}_{suc suc i}) (suc b)$
138	136 137	breq12d	$⊢ g = {f ↾}_{suc suc i} \to (g (b) R g (suc b) \leftrightarrow ({f ↾}_{suc suc i}) (b) R ({f ↾}_{suc suc i}) (suc b))$
139	138	ralbidv	$⊢ g = {f ↾}_{suc suc i} \to (\forall b \in suc i g (b) R g (suc b) \leftrightarrow \forall b \in suc i ({f ↾}_{suc suc i}) (b) R ({f ↾}_{suc suc i}) (suc b))$
140	130 135 139	3anbi123d	$⊢ g = {f ↾}_{suc suc i} \to ((g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b)) \leftrightarrow (({f ↾}_{suc suc i}) Fn suc suc i \land (({f ↾}_{suc suc i}) (\emptyset) = x \land ({f ↾}_{suc suc i}) (suc i) = f (suc i)) \land \forall b \in suc i ({f ↾}_{suc suc i}) (b) R ({f ↾}_{suc suc i}) (suc b)))$
141	129 140	spcev	$⊢ (({f ↾}_{suc suc i}) Fn suc suc i \land (({f ↾}_{suc suc i}) (\emptyset) = x \land ({f ↾}_{suc suc i}) (suc i) = f (suc i)) \land \forall b \in suc i ({f ↾}_{suc suc i}) (b) R ({f ↾}_{suc suc i}) (suc b)) \to \exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b))$
142	103 111 116 127 141	syl121anc	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to \exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b))$
143		simplrl	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to R \subseteq S$
144		simpr3	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to \forall a \in suc suc i f (a) R f (suc a)$
145		ssbr	$⊢ R \subseteq S \to (f (a) R f (suc a) \to f (a) S f (suc a))$
146	145	ralimdv	$⊢ R \subseteq S \to (\forall a \in suc suc i f (a) R f (suc a) \to \forall a \in suc suc i f (a) S f (suc a))$
147	143 144 146	sylc	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to \forall a \in suc suc i f (a) S f (suc a)$
148		fveq2	$⊢ a = suc i \to f (a) = f (suc i)$
149		suceq	$⊢ a = suc i \to suc a = suc suc i$
150	149	fveq2d	$⊢ a = suc i \to f (suc a) = f (suc suc i)$
151	148 150	breq12d	$⊢ a = suc i \to (f (a) S f (suc a) \leftrightarrow f (suc i) S f (suc suc i))$
152	151	rspcv	$⊢ suc i \in suc suc i \to (\forall a \in suc suc i f (a) S f (suc a) \to f (suc i) S f (suc suc i))$
153	114 147 152	mpsyl	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to f (suc i) S f (suc suc i)$
154		simpr2r	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to f (suc suc i) = y$
155	153 154	breqtrd	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to f (suc i) S y$
156		vex	$⊢ x \in V$
157		vex	$⊢ y \in V$
158	156 92 157	brcoi	$⊢ (x S f (suc i) \land f (suc i) S y) \to x (S \circ S) y$
159		simplrr	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to S \circ S \subseteq S$
160	159	ssbrd	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to (x (S \circ S) y \to x S y)$
161	158 160	syl5	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to ((x S f (suc i) \land f (suc i) S y) \to x S y)$
162	155 161	mpan2d	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to (x S f (suc i) \to x S y)$
163	142 162	embantd	$⊢ ((i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \land (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a))) \to ((\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b)) \to x S f (suc i)) \to x S y)$
164	163	ex	$⊢ (i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \to ((f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to ((\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b)) \to x S f (suc i)) \to x S y))$
165	164	com23	$⊢ (i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \to ((\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = f (suc i)) \land \forall b \in suc i g (b) R g (suc b)) \to x S f (suc i)) \to ((f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y))$
166	99 165	syl5	$⊢ (i \in ω \land (R \subseteq S \land S \circ S \subseteq S)) \to (\forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z) \to ((f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y))$
167	166	3impia	$⊢ (i \in ω \land (R \subseteq S \land S \circ S \subseteq S) \land \forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z)) \to ((f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y)$
168	167	exlimdv	$⊢ (i \in ω \land (R \subseteq S \land S \circ S \subseteq S) \land \forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z)) \to (\exists f (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y)$
169	168	alrimiv	$⊢ (i \in ω \land (R \subseteq S \land S \circ S \subseteq S) \land \forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z)) \to \forall y (\exists f (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y)$
170	169	3exp	$⊢ i \in ω \to ((R \subseteq S \land S \circ S \subseteq S) \to (\forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z) \to \forall y (\exists f (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y)))$
171	170	a2d	$⊢ i \in ω \to (((R \subseteq S \land S \circ S \subseteq S) \to \forall z (\exists g (g Fn suc suc i \land (g (\emptyset) = x \land g (suc i) = z) \land \forall b \in suc i g (b) R g (suc b)) \to x S z)) \to ((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc suc i \land (f (\emptyset) = x \land f (suc suc i) = y) \land \forall a \in suc suc i f (a) R f (suc a)) \to x S y)))$
172	23 61 72 83 91 171	finds	$⊢ n \in ω \to ((R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y))$
173	172	com12	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to (n \in ω \to \forall y (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y))$
174	173	ralrimiv	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to \forall n \in ω \forall y (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y)$
175		ralcom4	$⊢ \forall n \in ω \forall y (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y) \leftrightarrow \forall y \forall n \in ω (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y)$
176		r19.23v	$⊢ \forall n \in ω (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y) \leftrightarrow (\exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y)$
177	176	albii	$⊢ \forall y \forall n \in ω (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y) \leftrightarrow \forall y (\exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y)$
178	175 177	bitri	$⊢ \forall n \in ω \forall y (\exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y) \leftrightarrow \forall y (\exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y)$
179	174 178	sylib	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to \forall y (\exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y)$
180		brttrcl2	$⊢ x t++ R y \leftrightarrow \exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a))$
181		df-br	$⊢ x t++ R y \leftrightarrow ⟨x, y⟩ \in t++ R$
182	180 181	bitr3i	$⊢ \exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \leftrightarrow ⟨x, y⟩ \in t++ R$
183		df-br	$⊢ x S y \leftrightarrow ⟨x, y⟩ \in S$
184	182 183	imbi12i	$⊢ (\exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y) \leftrightarrow (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S)$
185	184	albii	$⊢ \forall y (\exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = x \land f (suc n) = y) \land \forall a \in suc n f (a) R f (suc a)) \to x S y) \leftrightarrow \forall y (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S)$
186	179 185	sylib	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to \forall y (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S)$
187	186	alrimiv	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to \forall x \forall y (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S)$
188		relttrcl	$⊢ Rel t++ R$
189		ssrel	$⊢ Rel t++ R \to (t++ R \subseteq S \leftrightarrow \forall x \forall y (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S))$
190	188 189	ax-mp	$⊢ t++ R \subseteq S \leftrightarrow \forall x \forall y (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S)$
191	187 190	sylibr	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to t++ R \subseteq S$

Metamath Proof Explorer

Theorem ttrclss

Proof