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