Metamath Proof Explorer

Theorem axcc2

Description: A possibly more useful version of ax-cc using sequences instead of countable sets. The Axiom of Infinity is needed to prove this, and indeed this implies the Axiom of Infinity. (Contributed by Mario Carneiro, 8-Feb-2013)

Ref Expression
Assertion axcc2 ⊢∃ggFnω∧∀n∈ωF⁡n≠∅→g⁡n∈F⁡n

Proof

Step Hyp Ref Expression
1 nfcv ⊢Ⅎ_nifF⁡m=∅∅F⁡m
2 nfcv ⊢Ⅎ_mifF⁡n=∅∅F⁡n
3 fveqeq2 ⊢m=n→F⁡m=∅↔F⁡n=∅
4 fveq2 ⊢m=n→F⁡m=F⁡n
5 3 4 ifbieq2d ⊢m=n→ifF⁡m=∅∅F⁡m=ifF⁡n=∅∅F⁡n
6 1 2 5 cbvmpt ⊢m∈ω⟼ifF⁡m=∅∅F⁡m=n∈ω⟼ifF⁡n=∅∅F⁡n
7 nfcv ⊢Ⅎ_nm×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m
8 nfcv ⊢Ⅎ_mn
9 nffvmpt1 ⊢Ⅎ_mm∈ω⟼ifF⁡m=∅∅F⁡m⁡n
10 8 9 nfxp ⊢Ⅎ_mn×m∈ω⟼ifF⁡m=∅∅F⁡m⁡n
11 sneq ⊢m=n→m=n
12 fveq2 ⊢m=n→m∈ω⟼ifF⁡m=∅∅F⁡m⁡m=m∈ω⟼ifF⁡m=∅∅F⁡m⁡n
13 11 12 xpeq12d ⊢m=n→m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m=n×m∈ω⟼ifF⁡m=∅∅F⁡m⁡n
14 7 10 13 cbvmpt ⊢m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m=n∈ω⟼n×m∈ω⟼ifF⁡m=∅∅F⁡m⁡n
15 nfcv ⊢Ⅎ_n2nd⁡f⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡m
16 nfcv ⊢Ⅎ_m2nd
17 nfcv ⊢Ⅎ_mf
18 nffvmpt1 ⊢Ⅎ_mm∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡n
19 17 18 nffv ⊢Ⅎ_mf⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡n
20 16 19 nffv ⊢Ⅎ_m2nd⁡f⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡n
21 2fveq3 ⊢m=n→f⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡m=f⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡n
22 21 fveq2d ⊢m=n→2nd⁡f⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡m=2nd⁡f⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡n
23 15 20 22 cbvmpt ⊢m∈ω⟼2nd⁡f⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡m=n∈ω⟼2nd⁡f⁡m∈ω⟼m×m∈ω⟼ifF⁡m=∅∅F⁡m⁡m⁡n
24 6 14 23 axcc2lem ⊢∃ggFnω∧∀n∈ωF⁡n≠∅→g⁡n∈F⁡n