Metamath Proof Explorer

Theorem brttrcl

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

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

Proof

Step Hyp Ref Expression
1 relttrcl ⊢ Rel t++ 𝑅
2 1 brrelex12i ⊢ ( 𝐴 t++ 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
3 fvex ⊢ ( 𝑓 ‘ ∅ ) ∈ V
4 eleq1 ⊢ ( ( 𝑓 ‘ ∅ ) = 𝐴 → ( ( 𝑓 ‘ ∅ ) ∈ V ↔ 𝐴 ∈ V ) )
5 3 4 mpbii ⊢ ( ( 𝑓 ‘ ∅ ) = 𝐴 → 𝐴 ∈ V )
6 fvex ⊢ ( 𝑓 ‘ 𝑛 ) ∈ V
7 eleq1 ⊢ ( ( 𝑓 ‘ 𝑛 ) = 𝐵 → ( ( 𝑓 ‘ 𝑛 ) ∈ V ↔ 𝐵 ∈ V ) )
8 6 7 mpbii ⊢ ( ( 𝑓 ‘ 𝑛 ) = 𝐵 → 𝐵 ∈ V )
9 5 8 anim12i ⊢ ( ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
10 9 3ad2ant2 ⊢ ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
11 10 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
12 11 rexlimivw ⊢ ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
13 eqeq2 ⊢ ( 𝑥 = 𝐴 → ( ( 𝑓 ‘ ∅ ) = 𝑥 ↔ ( 𝑓 ‘ ∅ ) = 𝐴 ) )
14 13 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ) )
15 14 3anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
16 15 exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
17 16 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
18 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( ( 𝑓 ‘ 𝑛 ) = 𝑦 ↔ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) )
19 18 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ) )
20 19 3anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
21 20 exbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
22 21 rexbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
23 df-ttrcl ⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
24 17 22 23 brabg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 t++ 𝑅 𝐵 ↔ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
25 2 12 24 pm5.21nii ⊢ ( 𝐴 t++ 𝑅 𝐵 ↔ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝐴 ∧ ( 𝑓 ‘ 𝑛 ) = 𝐵 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )