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 ⊢ ∃ g g Fn ω ∧ ∀ n ∈ ω F ⁡ n ≠ ∅ → g ⁡ n ∈ F ⁡ n

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ n if F ⁡ m = ∅ ∅ F ⁡ m
2 nfcv ⊢ Ⅎ _ m if F ⁡ 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 → if F ⁡ m = ∅ ∅ F ⁡ m = if F ⁡ n = ∅ ∅ F ⁡ n
6 1 2 5 cbvmpt ⊢ m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m = n ∈ ω ⟼ if F ⁡ n = ∅ ∅ F ⁡ n
7 nfcv ⊢ Ⅎ _ n m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m
8 nfcv ⊢ Ⅎ _ m n
9 nffvmpt1 ⊢ Ⅎ _ m m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ n
10 8 9 nfxp ⊢ Ⅎ _ m n × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ n
11 sneq ⊢ m = n → m = n
12 fveq2 ⊢ m = n → m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m = m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ n
13 11 12 xpeq12d ⊢ m = n → m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m = n × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ n
14 7 10 13 cbvmpt ⊢ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m = n ∈ ω ⟼ n × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ n
15 nfcv ⊢ Ⅎ _ n 2 nd ⁡ f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ m
16 nfcv ⊢ Ⅎ _ m 2 nd
17 nfcv ⊢ Ⅎ _ m f
18 nffvmpt1 ⊢ Ⅎ _ m m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ n
19 17 18 nffv ⊢ Ⅎ _ m f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ n
20 16 19 nffv ⊢ Ⅎ _ m 2 nd ⁡ f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ n
21 2fveq3 ⊢ m = n → f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ m = f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ n
22 21 fveq2d ⊢ m = n → 2 nd ⁡ f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ m = 2 nd ⁡ f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ n
23 15 20 22 cbvmpt ⊢ m ∈ ω ⟼ 2 nd ⁡ f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ m = n ∈ ω ⟼ 2 nd ⁡ f ⁡ m ∈ ω ⟼ m × m ∈ ω ⟼ if F ⁡ m = ∅ ∅ F ⁡ m ⁡ m ⁡ n
24 6 14 23 axcc2lem ⊢ ∃ g g Fn ω ∧ ∀ n ∈ ω F ⁡ n ≠ ∅ → g ⁡ n ∈ F ⁡ n