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 Could not format assertion : No typesetting found for |- ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 relttrcl Could not format Rel t++ R : No typesetting found for |- Rel t++ R with typecode |-
2 1 brrelex12i Could not format ( A t++ R B -> ( A e. _V /\ B e. _V ) ) : No typesetting found for |- ( A t++ R B -> ( A e. _V /\ B e. _V ) ) with typecode |-
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 Could not format t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } : No typesetting found for |- t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } with typecode |-
24 17 22 23 brabg Could not format ( ( A e. _V /\ B e. _V ) -> ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) ) : No typesetting found for |- ( ( A e. _V /\ B e. _V ) -> ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) ) with typecode |-
25 2 12 24 pm5.21nii Could not format ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) : No typesetting found for |- ( A t++ R B <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = A /\ ( f ` n ) = B ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) ) with typecode |-