ssttrcl

Description: If R is a relation, then it is a subclass of its transitive closure. (Contributed by Scott Fenton, 17-Oct-2024)

		Ref	Expression
	Assertion	ssttrcl	$⊢ Rel R \to R \subseteq t++ R$

Proof

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2		1on	$⊢ 1_{𝑜} \in On$
3	2	onirri	$⊢ \neg 1_{𝑜} \in 1_{𝑜}$
4		eldif	$⊢ 1_{𝑜} \in (ω ∖ 1_{𝑜}) \leftrightarrow (1_{𝑜} \in ω \land \neg 1_{𝑜} \in 1_{𝑜})$
5	1 3 4	mpbir2an	$⊢ 1_{𝑜} \in (ω ∖ 1_{𝑜})$
6		vex	$⊢ x \in V$
7		vex	$⊢ y \in V$
8	6 7	ifex	$⊢ if (m = \emptyset, x, y) \in V$
9		eqid	$⊢ (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y))$
10	8 9	fnmpti	$⊢ (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) Fn suc 1_{𝑜}$
11		eqid	$⊢ x = x$
12		eqid	$⊢ y = y$
13	11 12	pm3.2i	$⊢ (x = x \land y = y)$
14		1oex	$⊢ 1_{𝑜} \in V$
15	14	sucex	$⊢ suc 1_{𝑜} \in V$
16	15	mptex	$⊢ (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \in V$
17		fneq1	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to (f Fn suc 1_{𝑜} \leftrightarrow (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) Fn suc 1_{𝑜})$
18		fveq1	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to f (\emptyset) = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) (\emptyset)$
19	2	onordi	$⊢ Ord 1_{𝑜}$
20		0elsuc	$⊢ Ord 1_{𝑜} \to \emptyset \in suc 1_{𝑜}$
21	19 20	ax-mp	$⊢ \emptyset \in suc 1_{𝑜}$
22		iftrue	$⊢ m = \emptyset \to if (m = \emptyset, x, y) = x$
23	22 9 6	fvmpt	$⊢ \emptyset \in suc 1_{𝑜} \to (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) (\emptyset) = x$
24	21 23	ax-mp	$⊢ (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) (\emptyset) = x$
25	18 24	eqtrdi	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to f (\emptyset) = x$
26	25	eqeq1d	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to (f (\emptyset) = x \leftrightarrow x = x)$
27		fveq1	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to f (1_{𝑜}) = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) (1_{𝑜})$
28	14	sucid	$⊢ 1_{𝑜} \in suc 1_{𝑜}$
29		eqeq1	$⊢ m = 1_{𝑜} \to (m = \emptyset \leftrightarrow 1_{𝑜} = \emptyset)$
30	29	ifbid	$⊢ m = 1_{𝑜} \to if (m = \emptyset, x, y) = if (1_{𝑜} = \emptyset, x, y)$
31		1n0	$⊢ 1_{𝑜} \neq \emptyset$
32	31	neii	$⊢ \neg 1_{𝑜} = \emptyset$
33	32	iffalsei	$⊢ if (1_{𝑜} = \emptyset, x, y) = y$
34	33 7	eqeltri	$⊢ if (1_{𝑜} = \emptyset, x, y) \in V$
35	30 9 34	fvmpt	$⊢ 1_{𝑜} \in suc 1_{𝑜} \to (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) (1_{𝑜}) = if (1_{𝑜} = \emptyset, x, y)$
36	28 35	ax-mp	$⊢ (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) (1_{𝑜}) = if (1_{𝑜} = \emptyset, x, y)$
37	36 33	eqtri	$⊢ (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) (1_{𝑜}) = y$
38	27 37	eqtrdi	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to f (1_{𝑜}) = y$
39	38	eqeq1d	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to (f (1_{𝑜}) = y \leftrightarrow y = y)$
40	26 39	anbi12d	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to ((f (\emptyset) = x \land f (1_{𝑜}) = y) \leftrightarrow (x = x \land y = y))$
41	25 38	breq12d	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to (f (\emptyset) R f (1_{𝑜}) \leftrightarrow x R y)$
42	17 40 41	3anbi123d	$⊢ f = (m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) \to ((f Fn suc 1_{𝑜} \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})) \leftrightarrow ((m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) Fn suc 1_{𝑜} \land (x = x \land y = y) \land x R y))$
43	16 42	spcev	$⊢ ((m \in suc 1_{𝑜} ⟼ if (m = \emptyset, x, y)) Fn suc 1_{𝑜} \land (x = x \land y = y) \land x R y) \to \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜}))$
44	10 13 43	mp3an12	$⊢ x R y \to \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜}))$
45		suceq	$⊢ n = 1_{𝑜} \to suc n = suc 1_{𝑜}$
46	45	fneq2d	$⊢ n = 1_{𝑜} \to (f Fn suc n \leftrightarrow f Fn suc 1_{𝑜})$
47		fveqeq2	$⊢ n = 1_{𝑜} \to (f (n) = y \leftrightarrow f (1_{𝑜}) = y)$
48	47	anbi2d	$⊢ n = 1_{𝑜} \to ((f (\emptyset) = x \land f (n) = y) \leftrightarrow (f (\emptyset) = x \land f (1_{𝑜}) = y))$
49		raleq	$⊢ n = 1_{𝑜} \to (\forall m \in n f (m) R f (suc m) \leftrightarrow \forall m \in 1_{𝑜} f (m) R f (suc m))$
50		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
51	50	raleqi	$⊢ \forall m \in 1_{𝑜} f (m) R f (suc m) \leftrightarrow \forall m \in \{\emptyset\} f (m) R f (suc m)$
52		0ex	$⊢ \emptyset \in V$
53		fveq2	$⊢ m = \emptyset \to f (m) = f (\emptyset)$
54		suceq	$⊢ m = \emptyset \to suc m = suc \emptyset$
55		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
56	54 55	eqtr4di	$⊢ m = \emptyset \to suc m = 1_{𝑜}$
57	56	fveq2d	$⊢ m = \emptyset \to f (suc m) = f (1_{𝑜})$
58	53 57	breq12d	$⊢ m = \emptyset \to (f (m) R f (suc m) \leftrightarrow f (\emptyset) R f (1_{𝑜}))$
59	52 58	ralsn	$⊢ \forall m \in \{\emptyset\} f (m) R f (suc m) \leftrightarrow f (\emptyset) R f (1_{𝑜})$
60	51 59	bitri	$⊢ \forall m \in 1_{𝑜} f (m) R f (suc m) \leftrightarrow f (\emptyset) R f (1_{𝑜})$
61	49 60	bitrdi	$⊢ n = 1_{𝑜} \to (\forall m \in n f (m) R f (suc m) \leftrightarrow f (\emptyset) R f (1_{𝑜}))$
62	46 48 61	3anbi123d	$⊢ n = 1_{𝑜} \to ((f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m)) \leftrightarrow (f Fn suc 1_{𝑜} \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})))$
63	62	exbidv	$⊢ n = 1_{𝑜} \to (\exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m)) \leftrightarrow \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜})))$
64	63	rspcev	$⊢ (1_{𝑜} \in (ω ∖ 1_{𝑜}) \land \exists f (f Fn suc 1_{𝑜} \land (f (\emptyset) = x \land f (1_{𝑜}) = y) \land f (\emptyset) R f (1_{𝑜}))) \to \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m))$
65	5 44 64	sylancr	$⊢ x R y \to \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m))$
66		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
67		brttrcl	$⊢ x t++ R y \leftrightarrow \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m))$
68		df-br	$⊢ x t++ R y \leftrightarrow ⟨x, y⟩ \in t++ R$
69	67 68	bitr3i	$⊢ \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m)) \leftrightarrow ⟨x, y⟩ \in t++ R$
70	65 66 69	3imtr3i	$⊢ ⟨x, y⟩ \in R \to ⟨x, y⟩ \in t++ R$
71	70	gen2	$⊢ \forall x \forall y (⟨x, y⟩ \in R \to ⟨x, y⟩ \in t++ R)$
72		ssrel	$⊢ Rel R \to (R \subseteq t++ R \leftrightarrow \forall x \forall y (⟨x, y⟩ \in R \to ⟨x, y⟩ \in t++ R))$
73	71 72	mpbiri	$⊢ Rel R \to R \subseteq t++ R$

Metamath Proof Explorer

Theorem ssttrcl

Proof