Theorem ssttrcl 9755

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 8678	. . . . . 6 ⊢ 1o ∈ ω
2		1on 8518	. . . . . . 7 ⊢ 1o ∈ On
3	2	onirri 6497	. . . . . 6 ⊢ ¬ 1o ∈ 1o
4		eldif 3961	. . . . . 6 ⊢ (1o ∈ (ω ∖ 1o) ↔ (1o ∈ ω ∧ ¬ 1o ∈ 1o))
5	1, 3, 4	mpbir2an 711	. . . . 5 ⊢ 1o ∈ (ω ∖ 1o)
6		vex 3484	. . . . . . . 8 ⊢ 𝑥 ∈ V
7		vex 3484	. . . . . . . 8 ⊢ 𝑦 ∈ V
8	6, 7	ifex 4576	. . . . . . 7 ⊢ if(𝑚 = ∅, 𝑥, 𝑦) ∈ V
9		eqid 2737	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))
10	8, 9	fnmpti 6711	. . . . . 6 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o
11		eqid 2737	. . . . . . 7 ⊢ 𝑥 = 𝑥
12		eqid 2737	. . . . . . 7 ⊢ 𝑦 = 𝑦
13	11, 12	pm3.2i 470	. . . . . 6 ⊢ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)
14		1oex 8516	. . . . . . . . 9 ⊢ 1o ∈ V
15	14	sucex 7826	. . . . . . . 8 ⊢ suc 1o ∈ V
16	15	mptex 7243	. . . . . . 7 ⊢ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) ∈ V
17		fneq1 6659	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓 Fn suc 1o ↔ (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) Fn suc 1o))
18		fveq1 6905	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅))
19	2	onordi 6495	. . . . . . . . . . . . 13 ⊢ Ord 1o
20		0elsuc 7855	. . . . . . . . . . . . 13 ⊢ (Ord 1o → ∅ ∈ suc 1o)
21	19, 20	ax-mp 5	. . . . . . . . . . . 12 ⊢ ∅ ∈ suc 1o
22		iftrue 4531	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → if(𝑚 = ∅, 𝑥, 𝑦) = 𝑥)
23	22, 9, 6	fvmpt 7016	. . . . . . . . . . . 12 ⊢ (∅ ∈ suc 1o → ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅) = 𝑥)
24	21, 23	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘∅) = 𝑥
25	18, 24	eqtrdi 2793	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘∅) = 𝑥)
26	25	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘∅) = 𝑥 ↔ 𝑥 = 𝑥))
27		fveq1 6905	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o))
28	14	sucid 6466	. . . . . . . . . . . . 13 ⊢ 1o ∈ suc 1o
29		eqeq1 2741	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1o → (𝑚 = ∅ ↔ 1o = ∅))
30	29	ifbid 4549	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1o → if(𝑚 = ∅, 𝑥, 𝑦) = if(1o = ∅, 𝑥, 𝑦))
31		1n0 8526	. . . . . . . . . . . . . . . . 17 ⊢ 1o ≠ ∅
32	31	neii 2942	. . . . . . . . . . . . . . . 16 ⊢ ¬ 1o = ∅
33	32	iffalsei 4535	. . . . . . . . . . . . . . 15 ⊢ if(1o = ∅, 𝑥, 𝑦) = 𝑦
34	33, 7	eqeltri 2837	. . . . . . . . . . . . . 14 ⊢ if(1o = ∅, 𝑥, 𝑦) ∈ V
35	30, 9, 34	fvmpt 7016	. . . . . . . . . . . . 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 2765	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦))‘1o) = 𝑦
38	27, 37	eqtrdi 2793	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (𝑓‘1o) = 𝑦)
39	38	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → ((𝑓‘1o) = 𝑦 ↔ 𝑦 = 𝑦))
40	26, 39	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = (𝑚 ∈ suc 1o ↦ if(𝑚 = ∅, 𝑥, 𝑦)) → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦) ↔ (𝑥 = 𝑥 ∧ 𝑦 = 𝑦)))
41	25, 38	breq12d 5156	. . . . . . . 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 3606	. . . . . 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 6450	. . . . . . . . 9 ⊢ (𝑛 = 1o → suc 𝑛 = suc 1o)
46	45	fneq2d 6662	. . . . . . . 8 ⊢ (𝑛 = 1o → (𝑓 Fn suc 𝑛 ↔ 𝑓 Fn suc 1o))
47		fveqeq2 6915	. . . . . . . . 9 ⊢ (𝑛 = 1o → ((𝑓‘𝑛) = 𝑦 ↔ (𝑓‘1o) = 𝑦))
48	47	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = 1o → (((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ↔ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘1o) = 𝑦)))
49		raleq 3323	. . . . . . . . 9 ⊢ (𝑛 = 1o → (∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
50		df1o2 8513	. . . . . . . . . . 11 ⊢ 1o = {∅}
51	50	raleqi 3324	. . . . . . . . . 10 ⊢ (∀𝑚 ∈ 1o (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ ∀𝑚 ∈ {∅} (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))
52		0ex 5307	. . . . . . . . . . 11 ⊢ ∅ ∈ V
53		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘𝑚) = (𝑓‘∅))
54		suceq 6450	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → suc 𝑚 = suc ∅)
55		df-1o 8506	. . . . . . . . . . . . . 14 ⊢ 1o = suc ∅
56	54, 55	eqtr4di 2795	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → suc 𝑚 = 1o)
57	56	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (𝑓‘suc 𝑚) = (𝑓‘1o))
58	53, 57	breq12d 5156	. . . . . . . . . . 11 ⊢ (𝑚 = ∅ → ((𝑓‘𝑚)𝑅(𝑓‘suc 𝑚) ↔ (𝑓‘∅)𝑅(𝑓‘1o)))
59	52, 58	ralsn 4681	. . . . . . . . . 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 3622	. . . . 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 5144	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
67		brttrcl 9753	. . . . 5 ⊢ (𝑥t++𝑅𝑦 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚)))
68		df-br 5144	. . . . 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 5792	. 2 ⊢ (Rel 𝑅 → (𝑅 ⊆ t++𝑅 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ t++𝑅)))
73	71, 72	mpbiri 258	1 ⊢ (Rel 𝑅 → 𝑅 ⊆ t++𝑅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1087  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070  Vcvv 3480   ∖ cdif 3948   ⊆ wss 3951  ∅c0 4333  ifcif 4525  {csn 4626  ⟨cop 4632   class class class wbr 5143   ↦ cmpt 5225  Rel wrel 5690  Ord word 6383  suc csuc 6386   Fn wfn 6556  ‘cfv 6561  ωcom 7887  1_oc1o 8499  t++cttrcl 9747

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-1o 8506  df-ttrcl 9748

This theorem is referenced by:  ttrclco  9758  cottrcl  9759  dmttrcl  9761  rnttrcl  9762  dfttrcl2  9764  frmin  9789  frrlem16  9798  frr1  9799