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

Metamath Proof Explorer

Definition df-ttrcl

Description: Define the transitive closure of a class. This is the smallest relation containing R (or more precisely, the relation ` ( R |`_V ) induced by R ) and having the transitive property. Definition from Levy p. 59, who denotes it as R * and calls it the "ancestral" of R . (Contributed by Scott Fenton, 17-Oct-2024)

Ref Expression
Assertion df-ttrcl t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR ⊢ 𝑅
1 0 cttrcl ⊢ t++ 𝑅
2 vx ⊢ 𝑥
3 vy ⊢ 𝑦
4 vn ⊢ 𝑛
5 com ⊢ ω
6 c1o ⊢ 1o
7 5 6 cdif ⊢ ( ω ∖ 1o )
8 vf ⊢ 𝑓
9 8 cv ⊢ 𝑓
10 4 cv ⊢ 𝑛
11 10 csuc ⊢ suc 𝑛
12 9 11 wfn ⊢ 𝑓 Fn suc 𝑛
13 c0 ⊢ ∅
14 13 9 cfv ⊢ ( 𝑓 ‘ ∅ )
15 2 cv ⊢ 𝑥
16 14 15 wceq ⊢ ( 𝑓 ‘ ∅ ) = 𝑥
17 10 9 cfv ⊢ ( 𝑓 ‘ 𝑛 )
18 3 cv ⊢ 𝑦
19 17 18 wceq ⊢ ( 𝑓 ‘ 𝑛 ) = 𝑦
20 16 19 wa ⊢ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 )
21 vm ⊢ 𝑚
22 21 cv ⊢ 𝑚
23 22 9 cfv ⊢ ( 𝑓 ‘ 𝑚 )
24 22 csuc ⊢ suc 𝑚
25 24 9 cfv ⊢ ( 𝑓 ‘ suc 𝑚 )
26 23 25 0 wbr ⊢ ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 )
27 26 21 10 wral ⊢ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 )
28 12 20 27 w3a ⊢ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) )
29 28 8 wex ⊢ ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) )
30 29 4 7 wrex ⊢ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) )
31 30 2 3 copab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) }
32 1 31 wceq ⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) }