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 𝑎 ) ) )