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 𝐸 ) )