Metamath Proof Explorer

Theorem brttrcl2

Description: Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 24-Aug-2024)

Ref Expression
Assertion brttrcl2 ( 𝐴 t++ 𝑅 𝐵 ↔ ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )

Proof

Step Hyp Ref Expression
1 brttrcl ⊢ ( 𝐴 t++ 𝑅 𝐵 ↔ ∃ 𝑚 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
2 df-1o ⊢ 1o = suc ∅
3 2 difeq2i ⊢ ( ω ∖ 1o ) = ( ω ∖ suc ∅ )
4 3 eleq2i ⊢ ( 𝑚 ∈ ( ω ∖ 1o ) ↔ 𝑚 ∈ ( ω ∖ suc ∅ ) )
5 peano1 ⊢ ∅ ∈ ω
6 eldifsucnn ⊢ ( ∅ ∈ ω → ( 𝑚 ∈ ( ω ∖ suc ∅ ) ↔ ∃ 𝑛 ∈ ( ω ∖ ∅ ) 𝑚 = suc 𝑛 ) )
7 5 6 ax-mp ⊢ ( 𝑚 ∈ ( ω ∖ suc ∅ ) ↔ ∃ 𝑛 ∈ ( ω ∖ ∅ ) 𝑚 = suc 𝑛 )
8 dif0 ⊢ ( ω ∖ ∅ ) = ω
9 8 rexeqi ⊢ ( ∃ 𝑛 ∈ ( ω ∖ ∅ ) 𝑚 = suc 𝑛 ↔ ∃ 𝑛 ∈ ω 𝑚 = suc 𝑛 )
10 4 7 9 3bitri ⊢ ( 𝑚 ∈ ( ω ∖ 1o ) ↔ ∃ 𝑛 ∈ ω 𝑚 = suc 𝑛 )
11 10 anbi1i ⊢ ( ( 𝑚 ∈ ( ω ∖ 1o ) ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
12 r19.41v ⊢ ( ∃ 𝑛 ∈ ω ( 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
13 11 12 bitr4i ⊢ ( ( 𝑚 ∈ ( ω ∖ 1o ) ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ↔ ∃ 𝑛 ∈ ω ( 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
14 13 exbii ⊢ ( ∃ 𝑚 ( 𝑚 ∈ ( ω ∖ 1o ) ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ↔ ∃ 𝑚 ∃ 𝑛 ∈ ω ( 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
15 df-rex ⊢ ( ∃ 𝑚 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑚 ( 𝑚 ∈ ( ω ∖ 1o ) ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
16 rexcom4 ⊢ ( ∃ 𝑛 ∈ ω ∃ 𝑚 ( 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ↔ ∃ 𝑚 ∃ 𝑛 ∈ ω ( 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
17 14 15 16 3bitr4i ⊢ ( ∃ 𝑚 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑛 ∈ ω ∃ 𝑚 ( 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
18 vex ⊢ 𝑛 ∈ V
19 18 sucex ⊢ suc 𝑛 ∈ V
20 suceq ⊢ ( 𝑚 = suc 𝑛 → suc 𝑚 = suc suc 𝑛 )
21 20 fneq2d ⊢ ( 𝑚 = suc 𝑛 → ( 𝑓 Fn suc 𝑚 ↔ 𝑓 Fn suc suc 𝑛 ) )
22 fveqeq2 ⊢ ( 𝑚 = suc 𝑛 → ( ( 𝑓 ‘ 𝑚 ) = 𝐵 ↔ ( 𝑓 ‘ suc 𝑛 ) = 𝐵 ) )
23 22 anbi2d ⊢ ( 𝑚 = suc 𝑛 → ( ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝐵 ) ) )
24 raleq ⊢ ( 𝑚 = suc 𝑛 → ( ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
25 21 23 24 3anbi123d ⊢ ( 𝑚 = suc 𝑛 → ( ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
26 25 exbidv ⊢ ( 𝑚 = suc 𝑛 → ( ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
27 19 26 ceqsexv ⊢ ( ∃ 𝑚 ( 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
28 27 rexbii ⊢ ( ∃ 𝑛 ∈ ω ∃ 𝑚 ( 𝑚 = suc 𝑛 ∧ ∃ 𝑓 ( 𝑓 Fn suc 𝑚 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑚 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) ↔ ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
29 1 17 28 3bitri ⊢ ( 𝐴 t++ 𝑅 𝐵 ↔ ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ suc 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )