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 ⊢ A t++ R B ↔ ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a

Proof

Step Hyp Ref Expression
1 relttrcl ⊢ Rel ⁡ t++ R
2 1 brrelex12i ⊢ A t++ R B → A ∈ V ∧ B ∈ V
3 fvex ⊢ f ⁡ ∅ ∈ V
4 eleq1 ⊢ f ⁡ ∅ = A → f ⁡ ∅ ∈ V ↔ A ∈ V
5 3 4 mpbii ⊢ f ⁡ ∅ = A → A ∈ V
6 fvex ⊢ f ⁡ n ∈ V
7 eleq1 ⊢ f ⁡ n = B → f ⁡ n ∈ V ↔ B ∈ V
8 6 7 mpbii ⊢ f ⁡ n = B → B ∈ V
9 5 8 anim12i ⊢ f ⁡ ∅ = A ∧ f ⁡ n = B → A ∈ V ∧ B ∈ V
10 9 3ad2ant2 ⊢ f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a → A ∈ V ∧ B ∈ V
11 10 exlimiv ⊢ ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a → A ∈ V ∧ B ∈ V
12 11 rexlimivw ⊢ ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a → A ∈ V ∧ B ∈ V
13 eqeq2 ⊢ x = A → f ⁡ ∅ = x ↔ f ⁡ ∅ = A
14 13 anbi1d ⊢ x = A → f ⁡ ∅ = x ∧ f ⁡ n = y ↔ f ⁡ ∅ = A ∧ f ⁡ n = y
15 14 3anbi2d ⊢ x = A → f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a ↔ f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
16 15 exbidv ⊢ x = A → ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a ↔ ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
17 16 rexbidv ⊢ x = A → ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a ↔ ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
18 eqeq2 ⊢ y = B → f ⁡ n = y ↔ f ⁡ n = B
19 18 anbi2d ⊢ y = B → f ⁡ ∅ = A ∧ f ⁡ n = y ↔ f ⁡ ∅ = A ∧ f ⁡ n = B
20 19 3anbi2d ⊢ y = B → f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a ↔ f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
21 20 exbidv ⊢ y = B → ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a ↔ ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
22 21 rexbidv ⊢ y = B → ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a ↔ ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
23 df-ttrcl ⊢ t++ R = x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
24 17 22 23 brabg ⊢ A ∈ V ∧ B ∈ V → A t++ R B ↔ ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
25 2 12 24 pm5.21nii ⊢ A t++ R B ↔ ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = A ∧ f ⁡ n = B ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a