This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssttrcl

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

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

Proof

Step Hyp Ref Expression
1 1onn ⊢ 1o ∈ ω
2 1on ⊢ 1o ∈ On
3 2 onirri ⊢ ¬ 1o ∈ 1o
4 eldif ⊢ ( 1o ∈ ( ω ∖ 1o ) ↔ ( 1o ∈ ω ∧ ¬ 1o ∈ 1o ) )
5 1 3 4 mpbir2an ⊢ 1o ∈ ( ω ∖ 1o )
6 vex ⊢ 𝑥 ∈ V
7 vex ⊢ 𝑦 ∈ V
8 6 7 ifex ⊢ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ∈ V
9 eqid ⊢ ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) )
10 8 9 fnmpti ⊢ ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) Fn suc 1o
11 eqid ⊢ 𝑥 = 𝑥
12 eqid ⊢ 𝑦 = 𝑦
13 11 12 pm3.2i ⊢ ( 𝑥 = 𝑥 ∧ 𝑦 = 𝑦 )
14 1oex ⊢ 1o ∈ V
15 14 sucex ⊢ suc 1o ∈ V
16 15 mptex ⊢ ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) ∈ V
17 fneq1 ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( 𝑓 Fn suc 1o ↔ ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) Fn suc 1o ) )
18 fveq1 ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( 𝑓 ‘ ∅ ) = ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) ‘ ∅ ) )
19 2 onordi ⊢ Ord 1o
20 0elsuc ⊢ ( Ord 1o → ∅ ∈ suc 1o )
21 19 20 ax-mp ⊢ ∅ ∈ suc 1o
22 iftrue ⊢ ( 𝑚 = ∅ → if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) = 𝑥 )
23 22 9 6 fvmpt ⊢ ( ∅ ∈ suc 1o → ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) ‘ ∅ ) = 𝑥 )
24 21 23 ax-mp ⊢ ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) ‘ ∅ ) = 𝑥
25 18 24 eqtrdi ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( 𝑓 ‘ ∅ ) = 𝑥 )
26 25 eqeq1d ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( ( 𝑓 ‘ ∅ ) = 𝑥 ↔ 𝑥 = 𝑥 ) )
27 fveq1 ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( 𝑓 ‘ 1o ) = ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) ‘ 1o ) )
28 14 sucid ⊢ 1o ∈ suc 1o
29 eqeq1 ⊢ ( 𝑚 = 1o → ( 𝑚 = ∅ ↔ 1o = ∅ ) )
30 29 ifbid ⊢ ( 𝑚 = 1o → if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) = if ( 1o = ∅ , 𝑥 , 𝑦 ) )
31 1n0 ⊢ 1o ≠ ∅
32 31 neii ⊢ ¬ 1o = ∅
33 32 iffalsei ⊢ if ( 1o = ∅ , 𝑥 , 𝑦 ) = 𝑦
34 33 7 eqeltri ⊢ if ( 1o = ∅ , 𝑥 , 𝑦 ) ∈ V
35 30 9 34 fvmpt ⊢ ( 1o ∈ suc 1o → ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) ‘ 1o ) = if ( 1o = ∅ , 𝑥 , 𝑦 ) )
36 28 35 ax-mp ⊢ ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) ‘ 1o ) = if ( 1o = ∅ , 𝑥 , 𝑦 )
37 36 33 eqtri ⊢ ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) ‘ 1o ) = 𝑦
38 27 37 eqtrdi ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( 𝑓 ‘ 1o ) = 𝑦 )
39 38 eqeq1d ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( ( 𝑓 ‘ 1o ) = 𝑦 ↔ 𝑦 = 𝑦 ) )
40 26 39 anbi12d ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ↔ ( 𝑥 = 𝑥 ∧ 𝑦 = 𝑦 ) ) )
41 25 38 breq12d ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ↔ 𝑥 𝑅 𝑦 ) )
42 17 40 41 3anbi123d ⊢ ( 𝑓 = ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) → ( ( 𝑓 Fn suc 1o ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) ↔ ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) Fn suc 1o ∧ ( 𝑥 = 𝑥 ∧ 𝑦 = 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) )
43 16 42 spcev ⊢ ( ( ( 𝑚 ∈ suc 1o ↦ if ( 𝑚 = ∅ , 𝑥 , 𝑦 ) ) Fn suc 1o ∧ ( 𝑥 = 𝑥 ∧ 𝑦 = 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑓 ( 𝑓 Fn suc 1o ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) )
44 10 13 43 mp3an12 ⊢ ( 𝑥 𝑅 𝑦 → ∃ 𝑓 ( 𝑓 Fn suc 1o ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) )
45 suceq ⊢ ( 𝑛 = 1o → suc 𝑛 = suc 1o )
46 45 fneq2d ⊢ ( 𝑛 = 1o → ( 𝑓 Fn suc 𝑛 ↔ 𝑓 Fn suc 1o ) )
47 fveqeq2 ⊢ ( 𝑛 = 1o → ( ( 𝑓 ‘ 𝑛 ) = 𝑦 ↔ ( 𝑓 ‘ 1o ) = 𝑦 ) )
48 47 anbi2d ⊢ ( 𝑛 = 1o → ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ) )
49 raleq ⊢ ( 𝑛 = 1o → ( ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ↔ ∀ 𝑚 ∈ 1o ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) )
50 df1o2 ⊢ 1o = { ∅ }
51 50 raleqi ⊢ ( ∀ 𝑚 ∈ 1o ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ↔ ∀ 𝑚 ∈ { ∅ } ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) )
52 0ex ⊢ ∅ ∈ V
53 fveq2 ⊢ ( 𝑚 = ∅ → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ ∅ ) )
54 suceq ⊢ ( 𝑚 = ∅ → suc 𝑚 = suc ∅ )
55 df-1o ⊢ 1o = suc ∅
56 54 55 eqtr4di ⊢ ( 𝑚 = ∅ → suc 𝑚 = 1o )
57 56 fveq2d ⊢ ( 𝑚 = ∅ → ( 𝑓 ‘ suc 𝑚 ) = ( 𝑓 ‘ 1o ) )
58 53 57 breq12d ⊢ ( 𝑚 = ∅ → ( ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ↔ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) )
59 52 58 ralsn ⊢ ( ∀ 𝑚 ∈ { ∅ } ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ↔ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) )
60 51 59 bitri ⊢ ( ∀ 𝑚 ∈ 1o ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ↔ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) )
61 49 60 bitrdi ⊢ ( 𝑛 = 1o → ( ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ↔ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) )
62 46 48 61 3anbi123d ⊢ ( 𝑛 = 1o → ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) ↔ ( 𝑓 Fn suc 1o ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) ) )
63 62 exbidv ⊢ ( 𝑛 = 1o → ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc 1o ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) ) )
64 63 rspcev ⊢ ( ( 1o ∈ ( ω ∖ 1o ) ∧ ∃ 𝑓 ( 𝑓 Fn suc 1o ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 1o ) = 𝑦 ) ∧ ( 𝑓 ‘ ∅ ) 𝑅 ( 𝑓 ‘ 1o ) ) ) → ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) )
65 5 44 64 sylancr ⊢ ( 𝑥 𝑅 𝑦 → ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) )
66 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
67 brttrcl ⊢ ( 𝑥 t++ 𝑅 𝑦 ↔ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) )
68 df-br ⊢ ( 𝑥 t++ 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 )
69 67 68 bitr3i ⊢ ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 )
70 65 66 69 3imtr3i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 )
71 70 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 )
72 ssrel ⊢ ( Rel 𝑅 → ( 𝑅 ⊆ t++ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ t++ 𝑅 ) ) )
73 71 72 mpbiri ⊢ ( Rel 𝑅 → 𝑅 ⊆ t++ 𝑅 )