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

Metamath Proof Explorer

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 𝐴 ) )