Theorem 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	Could not format assertion : No typesetting found for |- ( Rel R -> R C_ t++ R ) with typecode |-

Proof

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