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 ω → E Fn ω
5 3 4 ax-mp ⊢ E Fn ω
6 fvelrnb ⊢ E Fn ω → 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 bitrid ⊢ 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 ⊢ E Fn ω → 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 bitrid ⊢ 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