Metamath Proof Explorer

Theorem axdc4uz

Description: A version of axdc4 that works on an upper set of integers instead of _om . (Contributed by Mario Carneiro, 8-Jan-2014)

Ref Expression
Hypotheses axdc4uz.1 ⊢ M ∈ ℤ
axdc4uz.2 ⊢ Z = ℤ ≥ M
Assertion axdc4uz ⊢ A ∈ V ∧ C ∈ A ∧ F : Z × A ⟶ 𝒫 A ∖ ∅ → ∃ g g : Z ⟶ A ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k

Proof

Step Hyp Ref Expression
1 axdc4uz.1 ⊢ M ∈ ℤ
2 axdc4uz.2 ⊢ Z = ℤ ≥ M
3 eleq2 ⊢ f = A → C ∈ f ↔ C ∈ A
4 xpeq2 ⊢ f = A → Z × f = Z × A
5 pweq ⊢ f = A → 𝒫 f = 𝒫 A
6 5 difeq1d ⊢ f = A → 𝒫 f ∖ ∅ = 𝒫 A ∖ ∅
7 4 6 feq23d ⊢ f = A → F : Z × f ⟶ 𝒫 f ∖ ∅ ↔ F : Z × A ⟶ 𝒫 A ∖ ∅
8 3 7 anbi12d ⊢ f = A → C ∈ f ∧ F : Z × f ⟶ 𝒫 f ∖ ∅ ↔ C ∈ A ∧ F : Z × A ⟶ 𝒫 A ∖ ∅
9 feq3 ⊢ f = A → g : Z ⟶ f ↔ g : Z ⟶ A
10 9 3anbi1d ⊢ f = A → g : Z ⟶ f ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k ↔ g : Z ⟶ A ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k
11 10 exbidv ⊢ f = A → ∃ g g : Z ⟶ f ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k ↔ ∃ g g : Z ⟶ A ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k
12 8 11 imbi12d ⊢ f = A → C ∈ f ∧ F : Z × f ⟶ 𝒫 f ∖ ∅ → ∃ g g : Z ⟶ f ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k ↔ C ∈ A ∧ F : Z × A ⟶ 𝒫 A ∖ ∅ → ∃ g g : Z ⟶ A ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k
13 vex ⊢ f ∈ V
14 eqid ⊢ rec ⁡ y ∈ V ⟼ y + 1 M ↾ ω = rec ⁡ y ∈ V ⟼ y + 1 M ↾ ω
15 eqid ⊢ n ∈ ω , x ∈ f ⟼ rec ⁡ y ∈ V ⟼ y + 1 M ↾ ω ⁡ n F x = n ∈ ω , x ∈ f ⟼ rec ⁡ y ∈ V ⟼ y + 1 M ↾ ω ⁡ n F x
16 1 2 13 14 15 axdc4uzlem ⊢ C ∈ f ∧ F : Z × f ⟶ 𝒫 f ∖ ∅ → ∃ g g : Z ⟶ f ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k
17 12 16 vtoclg ⊢ A ∈ V → C ∈ A ∧ F : Z × A ⟶ 𝒫 A ∖ ∅ → ∃ g g : Z ⟶ A ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k
18 17 3impib ⊢ A ∈ V ∧ C ∈ A ∧ F : Z × A ⟶ 𝒫 A ∖ ∅ → ∃ g g : Z ⟶ A ∧ g ⁡ M = C ∧ ∀ k ∈ Z g ⁡ k + 1 ∈ k F g ⁡ k