This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝑎 ∈ ω → ( ( 𝐸 ‘ 𝑎 ) = 𝐴 ↔ 𝐴 = ( 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 bitrid ⊢ ( 𝑎 ∈ ω → ( ( 𝐸 ‘ 𝑎 ) = 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 𝐸 ) )