Theorem numacn

Description: A well-orderable set has choice sequences of every length. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	numacn	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		simpll	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → 𝑋 ∈ dom card )
3		elmapi	⊢ ( 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) )
4	3	adantl	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → 𝑓 : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) )
5	4	frnd	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ran 𝑓 ⊆ ( 𝒫 𝑋 ∖ { ∅ } ) )
6	5	difss2d	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ran 𝑓 ⊆ 𝒫 𝑋 )
7		sspwuni	⊢ ( ran 𝑓 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝑓 ⊆ 𝑋 )
8	6 7	sylib	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∪ ran 𝑓 ⊆ 𝑋 )
9		ssnum	⊢ ( ( 𝑋 ∈ dom card ∧ ∪ ran 𝑓 ⊆ 𝑋 ) → ∪ ran 𝑓 ∈ dom card )
10	2 8 9	syl2anc	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∪ ran 𝑓 ∈ dom card )
11		ssdifin0	⊢ ( ran 𝑓 ⊆ ( 𝒫 𝑋 ∖ { ∅ } ) → ( ran 𝑓 ∩ { ∅ } ) = ∅ )
12	5 11	syl	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ( ran 𝑓 ∩ { ∅ } ) = ∅ )
13		disjsn	⊢ ( ( ran 𝑓 ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ran 𝑓 )
14	12 13	sylib	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ¬ ∅ ∈ ran 𝑓 )
15		ac5num	⊢ ( ( ∪ ran 𝑓 ∈ dom card ∧ ¬ ∅ ∈ ran 𝑓 ) → ∃ ℎ ( ℎ : ran 𝑓 ⟶ ∪ ran 𝑓 ∧ ∀ 𝑦 ∈ ran 𝑓 ( ℎ ‘ 𝑦 ) ∈ 𝑦 ) )
16	10 14 15	syl2anc	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∃ ℎ ( ℎ : ran 𝑓 ⟶ ∪ ran 𝑓 ∧ ∀ 𝑦 ∈ ran 𝑓 ( ℎ ‘ 𝑦 ) ∈ 𝑦 ) )
17		simpllr	⊢ ( ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( ℎ : ran 𝑓 ⟶ ∪ ran 𝑓 ∧ ∀ 𝑦 ∈ ran 𝑓 ( ℎ ‘ 𝑦 ) ∈ 𝑦 ) ) → 𝐴 ∈ V )
18	4	ffnd	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → 𝑓 Fn 𝐴 )
19		fveq2	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( ℎ ‘ 𝑦 ) = ( ℎ ‘ ( 𝑓 ‘ 𝑥 ) ) )
20		id	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → 𝑦 = ( 𝑓 ‘ 𝑥 ) )
21	19 20	eleq12d	⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( ( ℎ ‘ 𝑦 ) ∈ 𝑦 ↔ ( ℎ ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
22	21	ralrn	⊢ ( 𝑓 Fn 𝐴 → ( ∀ 𝑦 ∈ ran 𝑓 ( ℎ ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
23	18 22	syl	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ( ∀ 𝑦 ∈ ran 𝑓 ( ℎ ‘ 𝑦 ) ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
24	23	biimpa	⊢ ( ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ∀ 𝑦 ∈ ran 𝑓 ( ℎ ‘ 𝑦 ) ∈ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) )
25	24	adantrl	⊢ ( ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( ℎ : ran 𝑓 ⟶ ∪ ran 𝑓 ∧ ∀ 𝑦 ∈ ran 𝑓 ( ℎ ‘ 𝑦 ) ∈ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) )
26		acnlem	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) ) → ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
27	17 25 26	syl2anc	⊢ ( ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( ℎ : ran 𝑓 ⟶ ∪ ran 𝑓 ∧ ∀ 𝑦 ∈ ran 𝑓 ( ℎ ‘ 𝑦 ) ∈ 𝑦 ) ) → ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
28	16 27	exlimddv	⊢ ( ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) ∧ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
29	28	ralrimiva	⊢ ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) → ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
30		isacn	⊢ ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) → ( 𝑋 ∈ AC 𝐴 ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
31	29 30	mpbird	⊢ ( ( 𝑋 ∈ dom card ∧ 𝐴 ∈ V ) → 𝑋 ∈ AC 𝐴 )
32	31	expcom	⊢ ( 𝐴 ∈ V → ( 𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴 ) )
33	1 32	syl	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴 ) )