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		suceq	$⊢ suc m = suc \emptyset \to suc suc m = suc suc \emptyset$
3	1 2	syl	$⊢ m = \emptyset \to suc suc m = suc suc \emptyset$
4	3	fneq2d	$⊢ m = \emptyset \to (f Fn suc suc m \leftrightarrow f Fn suc suc \emptyset)$
5		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
6	1 5	eqtr4di	$⊢ m = \emptyset \to suc m = 1_{𝑜}$
7	6	fveqeq2d	$⊢ m = \emptyset \to (f (suc m) = y \leftrightarrow f (1_{𝑜}) = y)$
8	7	anbi2d	$⊢ m = \emptyset \to ((f (\emptyset) = x \land f (suc m) = y) \leftrightarrow (f (\emptyset) = x \land f (1_{𝑜}) = y))$
9		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
10	6 9	eqtrdi	$⊢ m = \emptyset \to suc m = \{\emptyset\}$
11	10	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))$
12		0ex	$⊢ \emptyset \in V$
13		fveq2	$⊢ a = \emptyset \to f (a) = f (\emptyset)$
14		suceq	$⊢ a = \emptyset \to suc a = suc \emptyset$
15	14 5	eqtr4di	$⊢ a = \emptyset \to suc a = 1_{𝑜}$
16	15	fveq2d	$⊢ a = \emptyset \to f (suc a) = f (1_{𝑜})$
17	13 16	breq12d	$⊢ a = \emptyset \to (f (a) R f (suc a) \leftrightarrow f (\emptyset) R f (1_{𝑜}))$
18	12 17	ralsn	$⊢ \forall a \in \{\emptyset\} f (a) R f (suc a) \leftrightarrow f (\emptyset) R f (1_{𝑜})$
19	11 18	bitrdi	$⊢ m = \emptyset \to (\forall a \in suc m f (a) R f (suc a) \leftrightarrow f (\emptyset) R f (1_{𝑜}))$
20	4 8 19	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_{𝑜})))$
21	20	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_{𝑜})))$
22	21	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))$
23	22	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))$
24	23	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)))$
25		suceq	$⊢ m = i \to suc m = suc i$
26		suceq	$⊢ suc m = suc i \to suc suc m = suc suc i$
27	25 26	syl	$⊢ m = i \to suc suc m = suc suc i$
28	27	fneq2d	$⊢ m = i \to (f Fn suc suc m \leftrightarrow f Fn suc suc i)$
29	25	fveqeq2d	$⊢ m = i \to (f (suc m) = y \leftrightarrow f (suc i) = y)$
30	29	anbi2d	$⊢ m = i \to ((f (\emptyset) = x \land f (suc m) = y) \leftrightarrow (f (\emptyset) = x \land f (suc i) = y))$
31	25	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))$
32		fveq2	$⊢ a = b \to f (a) = f (b)$
33		suceq	$⊢ a = b \to suc a = suc b$
34	33	fveq2d	$⊢ a = b \to f (suc a) = f (suc b)$
35	32 34	breq12d	$⊢ a = b \to (f (a) R f (suc a) \leftrightarrow f (b) R f (suc b))$
36	35	cbvralvw	$⊢ \forall a \in suc i f (a) R f (suc a) \leftrightarrow \forall b \in suc i f (b) R f (suc b)$
37	31 36	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))$
38	28 30 37	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)))$
39	38	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)))$
40		fneq1	$⊢ f = g \to (f Fn suc suc i \leftrightarrow g Fn suc suc i)$
41		fveq1	$⊢ f = g \to f (\emptyset) = g (\emptyset)$
42	41	eqeq1d	$⊢ f = g \to (f (\emptyset) = x \leftrightarrow g (\emptyset) = x)$
43		fveq1	$⊢ f = g \to f (suc i) = g (suc i)$
44	43	eqeq1d	$⊢ f = g \to (f (suc i) = y \leftrightarrow g (suc i) = y)$
45	42 44	anbi12d	$⊢ f = g \to ((f (\emptyset) = x \land f (suc i) = y) \leftrightarrow (g (\emptyset) = x \land g (suc i) = y))$
46		fveq1	$⊢ f = g \to f (b) = g (b)$
47		fveq1	$⊢ f = g \to f (suc b) = g (suc b)$
48	46 47	breq12d	$⊢ f = g \to (f (b) R f (suc b) \leftrightarrow g (b) R g (suc b))$
49	48	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))$
50	40 45 49	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)))$
51	50	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))$
52	39 51	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)))$
53	52	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))$
54	53	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))$
55		eqeq2	$⊢ y = z \to (g (suc i) = y \leftrightarrow g (suc i) = z)$
56	55	anbi2d	$⊢ y = z \to ((g (\emptyset) = x \land g (suc i) = y) \leftrightarrow (g (\emptyset) = x \land g (suc i) = z))$
57	56	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)))$
58	57	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)))$
59		breq2	$⊢ y = z \to (x S y \leftrightarrow x S z)$
60	58 59	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))$
61	60	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)$
62	54 61	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))$
63	62	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)))$
64		suceq	$⊢ m = suc i \to suc m = suc suc i$
65		suceq	$⊢ suc m = suc suc i \to suc suc m = suc suc suc i$
66	64 65	syl	$⊢ m = suc i \to suc suc m = suc suc suc i$
67	66	fneq2d	$⊢ m = suc i \to (f Fn suc suc m \leftrightarrow f Fn suc suc suc i)$
68	64	fveqeq2d	$⊢ m = suc i \to (f (suc m) = y \leftrightarrow f (suc suc i) = y)$
69	68	anbi2d	$⊢ m = suc i \to ((f (\emptyset) = x \land f (suc m) = y) \leftrightarrow (f (\emptyset) = x \land f (suc suc i) = y))$
70	64	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))$
71	67 69 70	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)))$
72	71	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)))$
73	72	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))$
74	73	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))$
75	74	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)))$
76		suceq	$⊢ m = n \to suc m = suc n$
77		suceq	$⊢ suc m = suc n \to suc suc m = suc suc n$
78	76 77	syl	$⊢ m = n \to suc suc m = suc suc n$
79	78	fneq2d	$⊢ m = n \to (f Fn suc suc m \leftrightarrow f Fn suc suc n)$
80	76	fveqeq2d	$⊢ m = n \to (f (suc m) = y \leftrightarrow f (suc n) = y)$
81	80	anbi2d	$⊢ m = n \to ((f (\emptyset) = x \land f (suc m) = y) \leftrightarrow (f (\emptyset) = x \land f (suc n) = y))$
82	76	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))$
83	79 81 82	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)))$
84	83	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)))$
85	84	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))$
86	85	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))$
87	86	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)))$
88		breq12	$⊢ (f (\emptyset) = x \land f (1_{𝑜}) = y) \to (f (\emptyset) R f (1_{𝑜}) \leftrightarrow x R y)$
89	88	biimpa	$⊢ ((f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x R y$
90	89	3adant1	$⊢ (f Fn suc suc \emptyset \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \to x R y$
91		ssbr	$⊢ R \subseteq S \to (x R y \to x S y)$
92	91	adantr	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to (x R y \to x S y)$
93	90 92	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)$
94	93	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)$
95	94	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)$
96		fvex	$⊢ f (suc i) \in V$
97		eqeq2	$⊢ z = f (suc i) \to (g (suc i) = z \leftrightarrow g (suc i) = f (suc i))$
98	97	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)))$
99	98	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)))$
100	99	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)))$
101		breq2	$⊢ z = f (suc i) \to (x S z \leftrightarrow x S f (suc i))$
102	100 101	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)))$
103	96 102	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))$
104		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$
105		sssucid	$⊢ suc suc i \subseteq suc suc suc i$
106		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$
107	104 105 106	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$
108		peano2	$⊢ i \in ω \to suc i \in ω$
109	108	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 ω$
110		nnord	$⊢ suc i \in ω \to Ord suc i$
111	109 110	syl	$⊢ ((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 Ord suc i$
112		0elsuc	$⊢ Ord suc i \to \emptyset \in suc suc i$
113	111 112	syl	$⊢ ((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$
114	113	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)$
115		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$
116	114 115	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$
117		vex	$⊢ i \in V$
118	117	sucex	$⊢ suc i \in V$
119	118	sucid	$⊢ suc i \in suc suc i$
120		fvres	$⊢ suc i \in suc suc i \to ({f ↾}_{suc suc i}) (suc i) = f (suc i)$
121	119 120	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)$
122		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)$
123		elelsuc	$⊢ b \in suc i \to b \in suc suc i$
124	123	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$
125	35 122 124	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)$
126	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}) (b) = f (b)$
127		ordsucelsuc	$⊢ Ord suc i \to (b \in suc i \leftrightarrow suc b \in suc suc i)$
128	111 127	syl	$⊢ ((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)$
129	128	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$
130	129	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)$
131	125 126 130	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)$
132	131	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)$
133		vex	$⊢ f \in V$
134	133	resex	$⊢ {f ↾}_{suc suc i} \in V$
135		fneq1	$⊢ g = {f ↾}_{suc suc i} \to (g Fn suc suc i \leftrightarrow ({f ↾}_{suc suc i}) Fn suc suc i)$
136		fveq1	$⊢ g = {f ↾}_{suc suc i} \to g (\emptyset) = ({f ↾}_{suc suc i}) (\emptyset)$
137	136	eqeq1d	$⊢ g = {f ↾}_{suc suc i} \to (g (\emptyset) = x \leftrightarrow ({f ↾}_{suc suc i}) (\emptyset) = x)$
138		fveq1	$⊢ g = {f ↾}_{suc suc i} \to g (suc i) = ({f ↾}_{suc suc i}) (suc i)$
139	138	eqeq1d	$⊢ g = {f ↾}_{suc suc i} \to (g (suc i) = f (suc i) \leftrightarrow ({f ↾}_{suc suc i}) (suc i) = f (suc i))$
140	137 139	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)))$
141		fveq1	$⊢ g = {f ↾}_{suc suc i} \to g (b) = ({f ↾}_{suc suc i}) (b)$
142		fveq1	$⊢ g = {f ↾}_{suc suc i} \to g (suc b) = ({f ↾}_{suc suc i}) (suc b)$
143	141 142	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))$
144	143	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))$
145	135 140 144	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)))$
146	134 145	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))$
147	107 116 121 132 146	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))$
148		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$
149		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)$
150		ssbr	$⊢ R \subseteq S \to (f (a) R f (suc a) \to f (a) S f (suc a))$
151	150	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))$
152	148 149 151	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)$
153		fveq2	$⊢ a = suc i \to f (a) = f (suc i)$
154		suceq	$⊢ a = suc i \to suc a = suc suc i$
155	154	fveq2d	$⊢ a = suc i \to f (suc a) = f (suc suc i)$
156	153 155	breq12d	$⊢ a = suc i \to (f (a) S f (suc a) \leftrightarrow f (suc i) S f (suc suc i))$
157	156	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))$
158	119 152 157	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)$
159		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$
160	158 159	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$
161		breq1	$⊢ z = f (suc i) \to (z S y \leftrightarrow f (suc i) S y)$
162	101 161	anbi12d	$⊢ z = f (suc i) \to ((x S z \land z S y) \leftrightarrow (x S f (suc i) \land f (suc i) S y))$
163	96 162	spcev	$⊢ (x S f (suc i) \land f (suc i) S y) \to \exists z (x S z \land z S y)$
164		vex	$⊢ x \in V$
165		vex	$⊢ y \in V$
166	164 165	brco	$⊢ x (S \circ S) y \leftrightarrow \exists z (x S z \land z S y)$
167	163 166	sylibr	$⊢ (x S f (suc i) \land f (suc i) S y) \to x (S \circ S) y$
168		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$
169	168	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)$
170	167 169	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)$
171	160 170	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)$
172	147 171	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)$
173	172	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))$
174	173	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))$
175	103 174	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))$
176	175	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)$
177	176	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)$
178	177	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)$
179	178	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)))$
180	179	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)))$
181	24 63 75 87 95 180	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))$
182	181	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))$
183	182	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)$
184		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)$
185		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)$
186	185	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)$
187	184 186	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)$
188	183 187	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)$
189		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))$
190		df-br	$⊢ x t++ R y \leftrightarrow ⟨x, y⟩ \in t++ R$
191	189 190	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$
192		df-br	$⊢ x S y \leftrightarrow ⟨x, y⟩ \in S$
193	191 192	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)$
194	193	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)$
195	188 194	sylib	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to \forall y (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S)$
196	195	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)$
197		relttrcl	$⊢ Rel t++ R$
198		ssrel	$⊢ Rel t++ R \to (t++ R \subseteq S \leftrightarrow \forall x \forall y (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S))$
199	197 198	ax-mp	$⊢ t++ R \subseteq S \leftrightarrow \forall x \forall y (⟨x, y⟩ \in t++ R \to ⟨x, y⟩ \in S)$
200	196 199	sylibr	$⊢ (R \subseteq S \land S \circ S \subseteq S) \to t++ R \subseteq S$

Metamath Proof Explorer

Theorem ttrclss

Proof