Metamath Proof Explorer

Theorem fin1a2lem5

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

Ref Expression
Hypothesis fin1a2lem.b ⊢E=x∈ω⟼2𝑜⋅𝑜x
Assertion fin1a2lem5 ⊢A∈ω→A∈ran⁡E↔¬suc⁡A∈ran⁡E

Proof

Step Hyp Ref Expression
1 fin1a2lem.b ⊢E=x∈ω⟼2𝑜⋅𝑜x
2 nneob ⊢A∈ω→∃a∈ωA=2𝑜⋅𝑜a↔¬∃a∈ωsuc⁡A=2𝑜⋅𝑜a
3 1 fin1a2lem4 ⊢E:ω⟶1-1ω
4 f1fn ⊢E:ω⟶1-1ω→EFnω
5 3 4 ax-mp ⊢EFnω
6 fvelrnb ⊢EFnω→A∈ran⁡E↔∃a∈ωE⁡a=A
7 5 6 ax-mp ⊢A∈ran⁡E↔∃a∈ωE⁡a=A
8 eqcom ⊢E⁡a=A↔A=E⁡a
9 1 fin1a2lem3 ⊢a∈ω→E⁡a=2𝑜⋅𝑜a
10 9 eqeq2d ⊢a∈ω→A=E⁡a↔A=2𝑜⋅𝑜a
11 8 10 syl5bb ⊢a∈ω→E⁡a=A↔A=2𝑜⋅𝑜a
12 11 rexbiia ⊢∃a∈ωE⁡a=A↔∃a∈ωA=2𝑜⋅𝑜a
13 7 12 bitri ⊢A∈ran⁡E↔∃a∈ωA=2𝑜⋅𝑜a
14 fvelrnb ⊢EFnω→suc⁡A∈ran⁡E↔∃a∈ωE⁡a=suc⁡A
15 5 14 ax-mp ⊢suc⁡A∈ran⁡E↔∃a∈ωE⁡a=suc⁡A
16 eqcom ⊢E⁡a=suc⁡A↔suc⁡A=E⁡a
17 9 eqeq2d ⊢a∈ω→suc⁡A=E⁡a↔suc⁡A=2𝑜⋅𝑜a
18 16 17 syl5bb ⊢a∈ω→E⁡a=suc⁡A↔suc⁡A=2𝑜⋅𝑜a
19 18 rexbiia ⊢∃a∈ωE⁡a=suc⁡A↔∃a∈ωsuc⁡A=2𝑜⋅𝑜a
20 15 19 bitri ⊢suc⁡A∈ran⁡E↔∃a∈ωsuc⁡A=2𝑜⋅𝑜a
21 20 notbii ⊢¬suc⁡A∈ran⁡E↔¬∃a∈ωsuc⁡A=2𝑜⋅𝑜a
22 2 13 21 3bitr4g ⊢A∈ω→A∈ran⁡E↔¬suc⁡A∈ran⁡E