Theorem ssttrcl 9753

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 8687	. . . . . 6 ⊢ 1o ∈ ω
2		1on 8527	. . . . . . 7 ⊢ 1o ∈ On
3	2	onirri 6503	. . . . . 6 ⊢ ¬ 1o ∈ 1o
4		eldif 4052	. . . . . 6 ⊢ (1o ∈ (ω ∖ 1o) ↔ (1o ∈ ω ∧ ¬ 1o ∈ 1o))
5	1, 3, 4	mpbir2an 724	. . . . 5 ⊢ 1o ∈ (ω ∖ 1o)
6		vex 3458	. . . . . . . 8 ⊢ 𝑥 ∈ V
7		vex 3458	. . . . . . . 8 ⊢ 𝑦 ∈ V
8	6, 7	ifex 4536	. . . . . . 7 ⊢ if(𝑚 = ∅, 𝑥, 𝑦) ∈ V
9		eqid 2763	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))
10	8, 9	fnmpti 6712	. . . . . 6 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o
11		eqid 2763	. . . . . . 7 ⊢ 𝑥 = 𝑥
12		eqid 2763	. . . . . . 7 ⊢ 𝑦 = 𝑦
13	11, 12	pm3.2i 476	. . . . . 6 ⊢ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)
14		1oex 8524	. . . . . . . . 9 ⊢ 1o ∈ V
15	14	sucex 7854	. . . . . . . 8 ⊢ suc 1o ∈ V
16	15	mptex 7260	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) ∈ V
17		fneq1 6660	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓 Fn suc 1o ↔ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o))
18		fveq1 6915	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅))
19	2	onordi 6502	. . . . . . . . . . . . 13 ⊢ Ord 1o
20		0elsuc 7880	. . . . . . . . . . . . 13 ⊢ (Ord 1o → ∅ ∈ suc 1o)
21	19, 20	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∅ ∈ suc 1o
22		iftrue 4491	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → if(𝑚 = ∅, 𝑥, 𝑦) = 𝑥)
23	22, 9, 6	fvmpt 7024	. . . . . . . . . . . 12 ⊢ (∅ ∈ suc 1o → ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅) = 𝑥)
24	21, 23	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅) = 𝑥
25	18, 24	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = 𝑥)
26	25	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘∅) = 𝑥 ↔ 𝑥 = 𝑥))
27		fveq1 6915	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o))
28	14	sucid 6473	. . . . . . . . . . . . 13 ⊢ 1o ∈ suc 1o
29		eqeq1 2767	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1o → (𝑚 = ∅ ↔ 1o = ∅))
30	29	ifbid 4509	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1o → if(𝑚 = ∅, 𝑥, 𝑦) = if(1o = ∅, 𝑥, 𝑦))
31		1n0 8533	. . . . . . . . . . . . . . . . 17 ⊢ 1o ≠ ∅
32	31	neii 2961	. . . . . . . . . . . . . . . 16 ⊢ ¬ 1o = ∅
33	32	iffalsei 4495	. . . . . . . . . . . . . . 15 ⊢ if(1o = ∅, 𝑥, 𝑦) = 𝑦
34	33, 7	eqeltri 2860	. . . . . . . . . . . . . 14 ⊢ if(1o = ∅, 𝑥, 𝑦) ∈ V
35	30, 9, 34	fvmpt 7024	. . . . . . . . . . . . 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 2786	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o) = 𝑦
38	27, 37	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = 𝑦)
39	38	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘1o) = 𝑦 ↔ 𝑦 = 𝑦))
40	26, 39	anbi12d 644	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)))
41	25, 38	breq12d 5121	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘∅)𝑅(𝑓‘1o) ↔ 𝑥𝑅𝑦))
42	17, 40, 41	3anbi123d 1465	. . . . . . 7 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)) ↔ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o ∧ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦) ∧ 𝑥𝑅𝑦)))
43	16, 42	spcev 3564	. . . . . 6 ⊢ (((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o ∧ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦) ∧ 𝑥𝑅𝑦) → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)))
44	10, 13, 43	mp3an12 1481	. . . . 5 ⊢ (𝑥𝑅𝑦 → ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o)))
45		suceq 6457	. . . . . . . . 9 ⊢ (𝑛 = 1o → suc 𝑛 = suc 1o)
46	45	fneq2d 6663	. . . . . . . 8 ⊢ (𝑛 = 1o → (𝑓 Fn suc 𝑛 ↔ 𝑓 Fn suc 1o))
47		fveqeq2 6925	. . . . . . . . 9 ⊢ (𝑛 = 1o → ((𝑓‘𝑛) = 𝑦 ↔ (𝑓‘1o) = 𝑦))
48	47	anbi2d 642	. . . . . . . 8 ⊢ (𝑛 = 1o → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦)))
49		raleq 3320	. . . . . . . . 9 ⊢ (𝑛 = 1o → (∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
50		df1o2 8521	. . . . . . . . . . 11 ⊢ 1o = {∅}
51	50	raleqi 3321	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ {∅} (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
52		0ex 5267	. . . . . . . . . . 11 ⊢ ∅ ∈ V
53		fveq2 6916	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘𝑚) = (𝑓‘∅))
54		suceq 6457	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
55		df-1o 8514	. . . . . . . . . . . . . 14 ⊢ 1o = suc ∅
56	54, 55	eqtr4di 2816	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → suc 𝑚 = 1o)
57	56	fveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘suc 𝑚) = (𝑓‘1o))
58	53, 57	breq12d 5121	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
59	52, 58	ralsn 4643	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ {∅} (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o))
60	51, 59	bitri 278	. . . . . . . . 9 ⊢ (∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o))
61	49, 60	bitrdi 290	. . . . . . . 8 ⊢ (𝑛 = 1o → (∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
62	46, 48, 61	3anbi123d 1465	. . . . . . 7 ⊢ (𝑛 = 1o → ((𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ (𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))))
63	62	exbidv 1956	. . . . . 6 ⊢ (𝑛 = 1o → (∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))))
64	63	rspcev 3580	. . . . 5 ⊢ ((1o ∈ (ω ∖ 1o) ∧ ∃𝑓(𝑓 Fn suc 1o ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ∧ (𝑓‘∅)𝑅(𝑓‘1o))) → ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
65	5, 44, 64	sylancr 599	. . . 4 ⊢ (𝑥𝑅𝑦 → ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
66		df-br 5109	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
67		brttrcl 9751	. . . . 5 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
68		df-br 5109	. . . . 5 ⊢ (𝑥t++𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
69	67, 68	bitr3i 280	. . . 4 ⊢ (∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)) ↔ ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
70	65, 66, 69	3imtr3i 294	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
71	70	gen2 1829	. 2 ⊢ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)
72		ssrel 5767	. 2 ⊢ (Rel 𝑅 → (𝑅 ⊆ t++𝑅 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)))
73	71, 72	mpbiri 261	1 ⊢ (Rel 𝑅 → 𝑅 ⊆ t++𝑅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048  ∅c0 4281  ifcif 4485  {csn 4588  ⟨cop 4840   class class class wbr 5108   ↦ cmpt 5192  Rel wrel 5663  Ord word 6387  suc csuc 6390   Fn wfn 6561  ‘cfv 6566  ωcom 7911  1_oc1o 8507  t++cttrcl 9745

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-om 7912  df-1o 8514  df-ttrcl 9746

This theorem is used by:  ttrclco  9756  cottrcl  9757  dmttrcl  9759  rnttrcl  9760  dfttrcl2  9762  frmin  9790  frrlem16  9799  frr1  9800