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

Proof

Step Hyp Ref Expression
1 brttrcl Could not format ( A t++ R B <-> E. m e. ( _om \ 1o ) E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) : No typesetting found for |- ( A t++ R B <-> E. m e. ( _om \ 1o ) E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) with typecode |-
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𝑜∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃n∈ωm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a
12 r19.41v ⊢∃n∈ωm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃n∈ωm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a
13 11 12 bitr4i ⊢m∈ω∖1𝑜∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃n∈ωm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a
14 13 exbii ⊢∃mm∈ω∖1𝑜∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃m∃n∈ωm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a
15 df-rex ⊢∃m∈ω∖1𝑜∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃mm∈ω∖1𝑜∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a
16 rexcom4 ⊢∃n∈ω∃mm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃m∃n∈ωm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a
17 14 15 16 3bitr4i ⊢∃m∈ω∖1𝑜∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃n∈ω∃mm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡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→fFnsuc⁡m↔fFnsuc⁡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∈mf⁡aRf⁡suc⁡a↔∀a∈suc⁡nf⁡aRf⁡suc⁡a
25 21 23 24 3anbi123d ⊢m=suc⁡n→fFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔fFnsuc⁡suc⁡n∧f⁡∅=A∧f⁡suc⁡n=B∧∀a∈suc⁡nf⁡aRf⁡suc⁡a
26 25 exbidv ⊢m=suc⁡n→∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃ffFnsuc⁡suc⁡n∧f⁡∅=A∧f⁡suc⁡n=B∧∀a∈suc⁡nf⁡aRf⁡suc⁡a
27 19 26 ceqsexv ⊢∃mm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃ffFnsuc⁡suc⁡n∧f⁡∅=A∧f⁡suc⁡n=B∧∀a∈suc⁡nf⁡aRf⁡suc⁡a
28 27 rexbii ⊢∃n∈ω∃mm=suc⁡n∧∃ffFnsuc⁡m∧f⁡∅=A∧f⁡m=B∧∀a∈mf⁡aRf⁡suc⁡a↔∃n∈ω∃ffFnsuc⁡suc⁡n∧f⁡∅=A∧f⁡suc⁡n=B∧∀a∈suc⁡nf⁡aRf⁡suc⁡a
29 1 17 28 3bitri Could not format ( A t++ R B <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) : No typesetting found for |- ( A t++ R B <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) with typecode |-