Theorem ssttrcl 9668

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 8604	. . . . . 6 ⊢ 1o ∈ ω
2		1on 8446	. . . . . . 7 ⊢ 1o ∈ On
3	2	onirri 6447	. . . . . 6 ⊢ ¬ 1o ∈ 1o
4		eldif 3924	. . . . . 6 ⊢ (1o ∈ (ω ∖ 1o) ↔ (1o ∈ ω ∧ ¬ 1o ∈ 1o))
5	1, 3, 4	mpbir2an 711	. . . . 5 ⊢ 1o ∈ (ω ∖ 1o)
6		vex 3451	. . . . . . . 8 ⊢ 𝑥 ∈ V
7		vex 3451	. . . . . . . 8 ⊢ 𝑦 ∈ V
8	6, 7	ifex 4539	. . . . . . 7 ⊢ if(𝑚 = ∅, 𝑥, 𝑦) ∈ V
9		eqid 2729	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))
10	8, 9	fnmpti 6661	. . . . . 6 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o
11		eqid 2729	. . . . . . 7 ⊢ 𝑥 = 𝑥
12		eqid 2729	. . . . . . 7 ⊢ 𝑦 = 𝑦
13	11, 12	pm3.2i 470	. . . . . 6 ⊢ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)
14		1oex 8444	. . . . . . . . 9 ⊢ 1o ∈ V
15	14	sucex 7782	. . . . . . . 8 ⊢ suc 1o ∈ V
16	15	mptex 7197	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) ∈ V
17		fneq1 6609	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓 Fn suc 1o ↔ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o))
18		fveq1 6857	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅))
19	2	onordi 6445	. . . . . . . . . . . . 13 ⊢ Ord 1o
20		0elsuc 7810	. . . . . . . . . . . . 13 ⊢ (Ord 1o → ∅ ∈ suc 1o)
21	19, 20	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∅ ∈ suc 1o
22		iftrue 4494	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → if(𝑚 = ∅, 𝑥, 𝑦) = 𝑥)
23	22, 9, 6	fvmpt 6968	. . . . . . . . . . . 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 6857	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o))
28	14	sucid 6416	. . . . . . . . . . . . 13 ⊢ 1o ∈ suc 1o
29		eqeq1 2733	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1o → (𝑚 = ∅ ↔ 1o = ∅))
30	29	ifbid 4512	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1o → if(𝑚 = ∅, 𝑥, 𝑦) = if(1o = ∅, 𝑥, 𝑦))
31		1n0 8452	. . . . . . . . . . . . . . . . 17 ⊢ 1o ≠ ∅
32	31	neii 2927	. . . . . . . . . . . . . . . 16 ⊢ ¬ 1o = ∅
33	32	iffalsei 4498	. . . . . . . . . . . . . . 15 ⊢ if(1o = ∅, 𝑥, 𝑦) = 𝑦
34	33, 7	eqeltri 2824	. . . . . . . . . . . . . 14 ⊢ if(1o = ∅, 𝑥, 𝑦) ∈ V
35	30, 9, 34	fvmpt 6968	. . . . . . . . . . . . 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 5120	. . . . . . . 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 3572	. . . . . 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 6400	. . . . . . . . 9 ⊢ (𝑛 = 1o → suc 𝑛 = suc 1o)
46	45	fneq2d 6612	. . . . . . . 8 ⊢ (𝑛 = 1o → (𝑓 Fn suc 𝑛 ↔ 𝑓 Fn suc 1o))
47		fveqeq2 6867	. . . . . . . . 9 ⊢ (𝑛 = 1o → ((𝑓‘𝑛) = 𝑦 ↔ (𝑓‘1o) = 𝑦))
48	47	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = 1o → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦)))
49		raleq 3296	. . . . . . . . 9 ⊢ (𝑛 = 1o → (∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
50		df1o2 8441	. . . . . . . . . . 11 ⊢ 1o = {∅}
51	50	raleqi 3297	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ {∅} (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
52		0ex 5262	. . . . . . . . . . 11 ⊢ ∅ ∈ V
53		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘𝑚) = (𝑓‘∅))
54		suceq 6400	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
55		df-1o 8434	. . . . . . . . . . . . . 14 ⊢ 1o = suc ∅
56	54, 55	eqtr4di 2782	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → suc 𝑚 = 1o)
57	56	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘suc 𝑚) = (𝑓‘1o))
58	53, 57	breq12d 5120	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
59	52, 58	ralsn 4645	. . . . . . . . . 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 3588	. . . . 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 5108	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
67		brttrcl 9666	. . . . 5 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
68		df-br 5108	. . . . 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 5745	. 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 3447   ∖ cdif 3911   ⊆ wss 3914  ∅c0 4296  ifcif 4488  {csn 4589  ⟨cop 4595   class class class wbr 5107   ↦ cmpt 5188  Rel wrel 5643  Ord word 6331  suc csuc 6334   Fn wfn 6506  ‘cfv 6511  ωcom 7842  1_oc1o 8427  t++cttrcl 9660

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 5234  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-om 7843  df-1o 8434  df-ttrcl 9661

This theorem is referenced by:  ttrclco  9671  cottrcl  9672  dmttrcl  9674  rnttrcl  9675  dfttrcl2  9677  frmin  9702  frrlem16  9711  frr1  9712