# Metamath Proof Explorer

## Theorem fin1a2lem5

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypothesis fin1a2lem.b 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
Assertion fin1a2lem5 ( 𝐴 ∈ ω → ( 𝐴 ∈ ran 𝐸 ↔ ¬ suc 𝐴 ∈ ran 𝐸 ) )

### Proof

Step Hyp Ref Expression
1 fin1a2lem.b 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
2 nneob ( 𝐴 ∈ ω → ( ∃ 𝑎 ∈ ω 𝐴 = ( 2o ·o 𝑎 ) ↔ ¬ ∃ 𝑎 ∈ ω suc 𝐴 = ( 2o ·o 𝑎 ) ) )
3 1 fin1a2lem4 𝐸 : ω –1-1→ ω
4 f1fn ( 𝐸 : ω –1-1→ ω → 𝐸 Fn ω )
5 3 4 ax-mp 𝐸 Fn ω
6 fvelrnb ( 𝐸 Fn ω → ( 𝐴 ∈ ran 𝐸 ↔ ∃ 𝑎 ∈ ω ( 𝐸𝑎 ) = 𝐴 ) )
7 5 6 ax-mp ( 𝐴 ∈ ran 𝐸 ↔ ∃ 𝑎 ∈ ω ( 𝐸𝑎 ) = 𝐴 )
8 eqcom ( ( 𝐸𝑎 ) = 𝐴𝐴 = ( 𝐸𝑎 ) )
9 1 fin1a2lem3 ( 𝑎 ∈ ω → ( 𝐸𝑎 ) = ( 2o ·o 𝑎 ) )
10 9 eqeq2d ( 𝑎 ∈ ω → ( 𝐴 = ( 𝐸𝑎 ) ↔ 𝐴 = ( 2o ·o 𝑎 ) ) )
11 8 10 syl5bb ( 𝑎 ∈ ω → ( ( 𝐸𝑎 ) = 𝐴𝐴 = ( 2o ·o 𝑎 ) ) )
12 11 rexbiia ( ∃ 𝑎 ∈ ω ( 𝐸𝑎 ) = 𝐴 ↔ ∃ 𝑎 ∈ ω 𝐴 = ( 2o ·o 𝑎 ) )
13 7 12 bitri ( 𝐴 ∈ ran 𝐸 ↔ ∃ 𝑎 ∈ ω 𝐴 = ( 2o ·o 𝑎 ) )
14 fvelrnb ( 𝐸 Fn ω → ( suc 𝐴 ∈ ran 𝐸 ↔ ∃ 𝑎 ∈ ω ( 𝐸𝑎 ) = suc 𝐴 ) )
15 5 14 ax-mp ( suc 𝐴 ∈ ran 𝐸 ↔ ∃ 𝑎 ∈ ω ( 𝐸𝑎 ) = suc 𝐴 )
16 eqcom ( ( 𝐸𝑎 ) = suc 𝐴 ↔ suc 𝐴 = ( 𝐸𝑎 ) )
17 9 eqeq2d ( 𝑎 ∈ ω → ( suc 𝐴 = ( 𝐸𝑎 ) ↔ suc 𝐴 = ( 2o ·o 𝑎 ) ) )
18 16 17 syl5bb ( 𝑎 ∈ ω → ( ( 𝐸𝑎 ) = suc 𝐴 ↔ suc 𝐴 = ( 2o ·o 𝑎 ) ) )
19 18 rexbiia ( ∃ 𝑎 ∈ ω ( 𝐸𝑎 ) = suc 𝐴 ↔ ∃ 𝑎 ∈ ω suc 𝐴 = ( 2o ·o 𝑎 ) )
20 15 19 bitri ( suc 𝐴 ∈ ran 𝐸 ↔ ∃ 𝑎 ∈ ω suc 𝐴 = ( 2o ·o 𝑎 ) )
21 20 notbii ( ¬ suc 𝐴 ∈ ran 𝐸 ↔ ¬ ∃ 𝑎 ∈ ω suc 𝐴 = ( 2o ·o 𝑎 ) )
22 2 13 21 3bitr4g ( 𝐴 ∈ ω → ( 𝐴 ∈ ran 𝐸 ↔ ¬ suc 𝐴 ∈ ran 𝐸 ) )