Theorem ssttrcl 9611

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 8558	. . . . . 6 ⊢ 1o ∈ ω
2		1on 8400	. . . . . . 7 ⊢ 1o ∈ On
3	2	onirri 6421	. . . . . 6 ⊢ ¬ 1o ∈ 1o
4		eldif 3913	. . . . . 6 ⊢ (1o ∈ (ω ∖ 1o) ↔ (1o ∈ ω ∧ ¬ 1o ∈ 1o))
5	1, 3, 4	mpbir2an 711	. . . . 5 ⊢ 1o ∈ (ω ∖ 1o)
6		vex 3440	. . . . . . . 8 ⊢ 𝑥 ∈ V
7		vex 3440	. . . . . . . 8 ⊢ 𝑦 ∈ V
8	6, 7	ifex 4527	. . . . . . 7 ⊢ if(𝑚 = ∅, 𝑥, 𝑦) ∈ V
9		eqid 2729	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))
10	8, 9	fnmpti 6625	. . . . . 6 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o
11		eqid 2729	. . . . . . 7 ⊢ 𝑥 = 𝑥
12		eqid 2729	. . . . . . 7 ⊢ 𝑦 = 𝑦
13	11, 12	pm3.2i 470	. . . . . 6 ⊢ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)
14		1oex 8398	. . . . . . . . 9 ⊢ 1o ∈ V
15	14	sucex 7742	. . . . . . . 8 ⊢ suc 1o ∈ V
16	15	mptex 7159	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) ∈ V
17		fneq1 6573	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓 Fn suc 1o ↔ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o))
18		fveq1 6821	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅))
19	2	onordi 6420	. . . . . . . . . . . . 13 ⊢ Ord 1o
20		0elsuc 7768	. . . . . . . . . . . . 13 ⊢ (Ord 1o → ∅ ∈ suc 1o)
21	19, 20	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∅ ∈ suc 1o
22		iftrue 4482	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → if(𝑚 = ∅, 𝑥, 𝑦) = 𝑥)
23	22, 9, 6	fvmpt 6930	. . . . . . . . . . . 12 ⊢ (∅ ∈ suc 1o → ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅) = 𝑥)
24	21, 23	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅) = 𝑥
25	18, 24	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = 𝑥)
26	25	eqeq1d 2731	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘∅) = 𝑥 ↔ 𝑥 = 𝑥))
27		fveq1 6821	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o))
28	14	sucid 6391	. . . . . . . . . . . . 13 ⊢ 1o ∈ suc 1o
29		eqeq1 2733	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1o → (𝑚 = ∅ ↔ 1o = ∅))
30	29	ifbid 4500	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1o → if(𝑚 = ∅, 𝑥, 𝑦) = if(1o = ∅, 𝑥, 𝑦))
31		1n0 8406	. . . . . . . . . . . . . . . . 17 ⊢ 1o ≠ ∅
32	31	neii 2927	. . . . . . . . . . . . . . . 16 ⊢ ¬ 1o = ∅
33	32	iffalsei 4486	. . . . . . . . . . . . . . 15 ⊢ if(1o = ∅, 𝑥, 𝑦) = 𝑦
34	33, 7	eqeltri 2824	. . . . . . . . . . . . . 14 ⊢ if(1o = ∅, 𝑥, 𝑦) ∈ V
35	30, 9, 34	fvmpt 6930	. . . . . . . . . . . . 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 2752	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o) = 𝑦
38	27, 37	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = 𝑦)
39	38	eqeq1d 2731	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘1o) = 𝑦 ↔ 𝑦 = 𝑦))
40	26, 39	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)))
41	25, 38	breq12d 5105	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘∅)𝑅(𝑓‘1o) ↔ 𝑥𝑅𝑦))
42	17, 40, 41	3anbi123d 1438	. . . . . . 7 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) ↔ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o ∧ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦) ∧ 𝑥𝑅𝑦)))
43	16, 42	spcev 3561	. . . . . 6 ⊢ (((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o ∧ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦) ∧ 𝑥𝑅𝑦) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)))
44	10, 13, 43	mp3an12 1453	. . . . 5 ⊢ (𝑥𝑅𝑦 → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)))
45		suceq 6375	. . . . . . . . 9 ⊢ (𝑛 = 1o → suc 𝑛 = suc 1o)
46	45	fneq2d 6576	. . . . . . . 8 ⊢ (𝑛 = 1o → (𝑓 Fn suc 𝑛 ↔ 𝑓 Fn suc 1o))
47		fveqeq2 6831	. . . . . . . . 9 ⊢ (𝑛 = 1o → ((𝑓‘𝑛) = 𝑦 ↔ (𝑓‘1o) = 𝑦))
48	47	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = 1o → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦)))
49		raleq 3286	. . . . . . . . 9 ⊢ (𝑛 = 1o → (∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
50		df1o2 8395	. . . . . . . . . . 11 ⊢ 1o = {∅}
51	50	raleqi 3287	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ {∅} (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
52		0ex 5246	. . . . . . . . . . 11 ⊢ ∅ ∈ V
53		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘𝑚) = (𝑓‘∅))
54		suceq 6375	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
55		df-1o 8388	. . . . . . . . . . . . . 14 ⊢ 1o = suc ∅
56	54, 55	eqtr4di 2782	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → suc 𝑚 = 1o)
57	56	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘suc 𝑚) = (𝑓‘1o))
58	53, 57	breq12d 5105	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
59	52, 58	ralsn 4633	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ {∅} (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o))
60	51, 59	bitri 275	. . . . . . . . 9 ⊢ (∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o))
61	49, 60	bitrdi 287	. . . . . . . 8 ⊢ (𝑛 = 1o → (∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
62	46, 48, 61	3anbi123d 1438	. . . . . . 7 ⊢ (𝑛 = 1o → ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))))
63	62	exbidv 1921	. . . . . 6 ⊢ (𝑛 = 1o → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))))
64	63	rspcev 3577	. . . . 5 ⊢ ((1o ∈ (ω ∖ 1o) ∧ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))) → ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
65	5, 44, 64	sylancr 587	. . . 4 ⊢ (𝑥𝑅𝑦 → ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
66		df-br 5093	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
67		brttrcl 9609	. . . . 5 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
68		df-br 5093	. . . . 5 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
69	67, 68	bitr3i 277	. . . 4 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
70	65, 66, 69	3imtr3i 291	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
71	70	gen2 1796	. 2 ⊢ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
72		ssrel 5726	. 2 ⊢ (Rel 𝑅 → (𝑅 ⊆ t++𝑅 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)))
73	71, 72	mpbiri 258	1 ⊢ (Rel 𝑅 → 𝑅 ⊆ t++𝑅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  Vcvv 3436   ∖ cdif 3900   ⊆ wss 3903  ∅c0 4284  ifcif 4476  {csn 4577  ⟨cop 4583   class class class wbr 5092   ↦ cmpt 5173  Rel wrel 5624  Ord word 6306  suc csuc 6309   Fn wfn 6477  ‘cfv 6482  ωcom 7799  1_oc1o 8381  t++cttrcl 9603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-om 7800  df-1o 8388  df-ttrcl 9604

This theorem is referenced by:  ttrclco  9614  cottrcl  9615  dmttrcl  9617  rnttrcl  9618  dfttrcl2  9620  frmin  9645  frrlem16  9654  frr1  9655