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∖∅→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡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∈Zg⁡k+1∈kFg⁡k↔g:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k
11 10 exbidv ⊢f=A→∃gg:Z⟶f∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k↔∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k
12 8 11 imbi12d ⊢f=A→C∈f∧F:Z×f⟶𝒫f∖∅→∃gg:Z⟶f∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k↔C∈A∧F:Z×A⟶𝒫A∖∅→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k
13 vex ⊢f∈V
14 eqid ⊢rec⁡y∈V⟼y+1M↾ω=rec⁡y∈V⟼y+1M↾ω
15 eqid ⊢n∈ω,x∈f⟼rec⁡y∈V⟼y+1M↾ω⁡nFx=n∈ω,x∈f⟼rec⁡y∈V⟼y+1M↾ω⁡nFx
16 1 2 13 14 15 axdc4uzlem ⊢C∈f∧F:Z×f⟶𝒫f∖∅→∃gg:Z⟶f∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k
17 12 16 vtoclg ⊢A∈V→C∈A∧F:Z×A⟶𝒫A∖∅→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k
18 17 3impib ⊢A∈V∧C∈A∧F:Z×A⟶𝒫A∖∅→∃gg:Z⟶A∧g⁡M=C∧∀k∈Zg⁡k+1∈kFg⁡k