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	⊢ ( Rel 𝑅 → 𝑅 ⊆ t++ 𝑅 )

Proof

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