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

Proof

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