Theorem ssttrcl 33701

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

Assertion

Ref	Expression
ssttrcl	⊢ (Rel 𝑅 → 𝑅 ⊆ t++𝑅)

Proof of Theorem ssttrcl

Dummy variables 𝑥 𝑦 𝑓 𝑛 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1onn 8432	. . . . . 6 ⊢ 1o ∈ ω
2		1on 8274	. . . . . . 7 ⊢ 1o ∈ On
3	2	onirri 6358	. . . . . 6 ⊢ ¬ 1o ∈ 1o
4		eldif 3893	. . . . . 6 ⊢ (1o ∈ (ω ∖ 1o) ↔ (1o ∈ ω ∧ ¬ 1o ∈ 1o))
5	1, 3, 4	mpbir2an 707	. . . . 5 ⊢ 1o ∈ (ω ∖ 1o)
6		vex 3426	. . . . . . . 8 ⊢ 𝑥 ∈ V
7		vex 3426	. . . . . . . 8 ⊢ 𝑦 ∈ V
8	6, 7	ifex 4506	. . . . . . 7 ⊢ if(𝑚 = ∅, 𝑥, 𝑦) ∈ V
9		eqid 2738	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))
10	8, 9	fnmpti 6560	. . . . . 6 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o
11		eqid 2738	. . . . . . 7 ⊢ 𝑥 = 𝑥
12		eqid 2738	. . . . . . 7 ⊢ 𝑦 = 𝑦
13	11, 12	pm3.2i 470	. . . . . 6 ⊢ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)
14		1oex 8280	. . . . . . . . 9 ⊢ 1o ∈ V
15	14	sucex 7633	. . . . . . . 8 ⊢ suc 1o ∈ V
16	15	mptex 7081	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) ∈ V
17		fneq1 6508	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓 Fn suc 1o ↔ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o))
18		fveq1 6755	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅))
19	2	onordi 6356	. . . . . . . . . . . . 13 ⊢ Ord 1o
20		0elsuc 7657	. . . . . . . . . . . . 13 ⊢ (Ord 1o → ∅ ∈ suc 1o)
21	19, 20	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∅ ∈ suc 1o
22		iftrue 4462	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → if(𝑚 = ∅, 𝑥, 𝑦) = 𝑥)
23	22, 9, 6	fvmpt 6857	. . . . . . . . . . . 12 ⊢ (∅ ∈ suc 1o → ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅) = 𝑥)
24	21, 23	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅) = 𝑥
25	18, 24	eqtrdi 2795	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = 𝑥)
26	25	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘∅) = 𝑥 ↔ 𝑥 = 𝑥))
27		fveq1 6755	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o))
28	14	sucid 6330	. . . . . . . . . . . . 13 ⊢ 1o ∈ suc 1o
29		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1o → (𝑚 = ∅ ↔ 1o = ∅))
30	29	ifbid 4479	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1o → if(𝑚 = ∅, 𝑥, 𝑦) = if(1o = ∅, 𝑥, 𝑦))
31		1n0 8286	. . . . . . . . . . . . . . . . 17 ⊢ 1o ≠ ∅
32	31	neii 2944	. . . . . . . . . . . . . . . 16 ⊢ ¬ 1o = ∅
33	32	iffalsei 4466	. . . . . . . . . . . . . . 15 ⊢ if(1o = ∅, 𝑥, 𝑦) = 𝑦
34	33, 7	eqeltri 2835	. . . . . . . . . . . . . 14 ⊢ if(1o = ∅, 𝑥, 𝑦) ∈ V
35	30, 9, 34	fvmpt 6857	. . . . . . . . . . . . 13 ⊢ (1o ∈ suc 1o → ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o) = if(1o = ∅, 𝑥, 𝑦))
36	28, 35	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o) = if(1o = ∅, 𝑥, 𝑦)
37	36, 33	eqtri 2766	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o) = 𝑦
38	27, 37	eqtrdi 2795	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = 𝑦)
39	38	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘1o) = 𝑦 ↔ 𝑦 = 𝑦))
40	26, 39	anbi12d 630	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)))
41	25, 38	breq12d 5083	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘∅)𝑅(𝑓‘1o) ↔ 𝑥𝑅𝑦))
42	17, 40, 41	3anbi123d 1434	. . . . . . 7 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) ↔ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o ∧ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦) ∧ 𝑥𝑅𝑦)))
43	16, 42	spcev 3535	. . . . . 6 ⊢ (((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o ∧ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦) ∧ 𝑥𝑅𝑦) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)))
44	10, 13, 43	mp3an12 1449	. . . . 5 ⊢ (𝑥𝑅𝑦 → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)))
45		suceq 6316	. . . . . . . . 9 ⊢ (𝑛 = 1o → suc 𝑛 = suc 1o)
46	45	fneq2d 6511	. . . . . . . 8 ⊢ (𝑛 = 1o → (𝑓 Fn suc 𝑛 ↔ 𝑓 Fn suc 1o))
47		fveqeq2 6765	. . . . . . . . 9 ⊢ (𝑛 = 1o → ((𝑓‘𝑛) = 𝑦 ↔ (𝑓‘1o) = 𝑦))
48	47	anbi2d 628	. . . . . . . 8 ⊢ (𝑛 = 1o → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦)))
49		raleq 3333	. . . . . . . . 9 ⊢ (𝑛 = 1o → (∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
50		df1o2 8279	. . . . . . . . . . 11 ⊢ 1o = {∅}
51	50	raleqi 3337	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ {∅} (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
52		0ex 5226	. . . . . . . . . . 11 ⊢ ∅ ∈ V
53		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘𝑚) = (𝑓‘∅))
54		suceq 6316	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
55		df-1o 8267	. . . . . . . . . . . . . 14 ⊢ 1o = suc ∅
56	54, 55	eqtr4di 2797	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → suc 𝑚 = 1o)
57	56	fveq2d 6760	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘suc 𝑚) = (𝑓‘1o))
58	53, 57	breq12d 5083	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
59	52, 58	ralsn 4614	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ {∅} (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o))
60	51, 59	bitri 274	. . . . . . . . 9 ⊢ (∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o))
61	49, 60	bitrdi 286	. . . . . . . 8 ⊢ (𝑛 = 1o → (∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
62	46, 48, 61	3anbi123d 1434	. . . . . . 7 ⊢ (𝑛 = 1o → ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))))
63	62	exbidv 1925	. . . . . 6 ⊢ (𝑛 = 1o → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))))
64	63	rspcev 3552	. . . . 5 ⊢ ((1o ∈ (ω ∖ 1o) ∧ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))) → ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
65	5, 44, 64	sylancr 586	. . . 4 ⊢ (𝑥𝑅𝑦 → ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
66		df-br 5071	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
67		brttrcl 33699	. . . . 5 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
68		df-br 5071	. . . . 5 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
69	67, 68	bitr3i 276	. . . 4 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
70	65, 66, 69	3imtr3i 290	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
71	70	gen2 1800	. 2 ⊢ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
72		ssrel 5683	. 2 ⊢ (Rel 𝑅 → (𝑅 ⊆ t++𝑅 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)))
73	71, 72	mpbiri 257	1 ⊢ (Rel 𝑅 → 𝑅 ⊆ t++𝑅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  Vcvv 3422   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4253  ifcif 4456  {csn 4558  ⟨cop 4564   class class class wbr 5070   ↦ cmpt 5153  Rel wrel 5585  Ord word 6250  suc csuc 6253   Fn wfn 6413  ‘cfv 6418  ωcom 7687  1_oc1o 8260  t++cttrcl 33693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-om 7688  df-1o 8267  df-ttrcl 33694

This theorem is referenced by:  ttrclco  33704  cottrcl  33705  dmttrcl  33707  rnttrcl  33708  dfttrcl2  33710