This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ 𝑛 if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) )
2 nfcv ⊢ Ⅎ 𝑚 if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) )
3 fveqeq2 ⊢ ( 𝑚 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) = ∅ ↔ ( 𝐹 ‘ 𝑛 ) = ∅ ) )
4 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
5 3 4 ifbieq2d ⊢ ( 𝑚 = 𝑛 → if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) = if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) )
6 1 2 5 cbvmpt ⊢ ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) = ( 𝑛 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑛 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑛 ) ) )
7 nfcv ⊢ Ⅎ 𝑛 ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) )
8 nfcv ⊢ Ⅎ 𝑚 { 𝑛 }
9 nffvmpt1 ⊢ Ⅎ 𝑚 ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑛 )
10 8 9 nfxp ⊢ Ⅎ 𝑚 ( { 𝑛 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑛 ) )
11 sneq ⊢ ( 𝑚 = 𝑛 → { 𝑚 } = { 𝑛 } )
12 fveq2 ⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) = ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑛 ) )
13 11 12 xpeq12d ⊢ ( 𝑚 = 𝑛 → ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) = ( { 𝑛 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑛 ) ) )
14 7 10 13 cbvmpt ⊢ ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) = ( 𝑛 ∈ ω ↦ ( { 𝑛 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑛 ) ) )
15 nfcv ⊢ Ⅎ 𝑛 ( 2nd ‘ ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) )
16 nfcv ⊢ Ⅎ 𝑚 2nd
17 nfcv ⊢ Ⅎ 𝑚 𝑓
18 nffvmpt1 ⊢ Ⅎ 𝑚 ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑛 )
19 17 18 nffv ⊢ Ⅎ 𝑚 ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) )
20 16 19 nffv ⊢ Ⅎ 𝑚 ( 2nd ‘ ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) ) )
21 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) = ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) ) )
22 21 fveq2d ⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) = ( 2nd ‘ ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) ) ) )
23 15 20 22 cbvmpt ⊢ ( 𝑚 ∈ ω ↦ ( 2nd ‘ ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ) = ( 𝑛 ∈ ω ↦ ( 2nd ‘ ( 𝑓 ‘ ( ( 𝑚 ∈ ω ↦ ( { 𝑚 } × ( ( 𝑚 ∈ ω ↦ if ( ( 𝐹 ‘ 𝑚 ) = ∅ , { ∅ } , ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑚 ) ) ) ‘ 𝑛 ) ) ) )
24 6 14 23 axcc2lem ⊢ ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑛 ∈ ω ( ( 𝐹 ‘ 𝑛 ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( 𝐹 ‘ 𝑛 ) ) )