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

Metamath Proof Explorer

Theorem acndom2

Description: A set smaller than one with choice sequences of length A also has choice sequences of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acndom2 ( 𝑋 ≼ 𝑌 → ( 𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴 ) )

Proof

Step Hyp Ref Expression
1 brdomi ⊢ ( 𝑋 ≼ 𝑌 → ∃ 𝑓 𝑓 : 𝑋 –1-1→ 𝑌 )
2 simplr ⊢ ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → 𝑌 ∈ AC 𝐴 )
3 imassrn ⊢ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ⊆ ran 𝑓
4 simplll ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑓 : 𝑋 –1-1→ 𝑌 )
5 f1f ⊢ ( 𝑓 : 𝑋 –1-1→ 𝑌 → 𝑓 : 𝑋 ⟶ 𝑌 )
6 frn ⊢ ( 𝑓 : 𝑋 ⟶ 𝑌 → ran 𝑓 ⊆ 𝑌 )
7 4 5 6 3syl ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ran 𝑓 ⊆ 𝑌 )
8 3 7 sstrid ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ⊆ 𝑌 )
9 elmapi ⊢ ( 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) → 𝑔 : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) )
10 9 adantl ⊢ ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → 𝑔 : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) )
11 10 ffvelcdmda ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ { ∅ } ) )
12 11 eldifad ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝒫 𝑋 )
13 12 elpwid ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ⊆ 𝑋 )
14 f1dm ⊢ ( 𝑓 : 𝑋 –1-1→ 𝑌 → dom 𝑓 = 𝑋 )
15 4 14 syl ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → dom 𝑓 = 𝑋 )
16 13 15 sseqtrrd ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ⊆ dom 𝑓 )
17 sseqin2 ⊢ ( ( 𝑔 ‘ 𝑥 ) ⊆ dom 𝑓 ↔ ( dom 𝑓 ∩ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑔 ‘ 𝑥 ) )
18 16 17 sylib ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( dom 𝑓 ∩ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑔 ‘ 𝑥 ) )
19 eldifsni ⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ ( 𝒫 𝑋 ∖ { ∅ } ) → ( 𝑔 ‘ 𝑥 ) ≠ ∅ )
20 11 19 syl ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ≠ ∅ )
21 18 20 eqnetrd ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( dom 𝑓 ∩ ( 𝑔 ‘ 𝑥 ) ) ≠ ∅ )
22 imadisj ⊢ ( ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) = ∅ ↔ ( dom 𝑓 ∩ ( 𝑔 ‘ 𝑥 ) ) = ∅ )
23 22 necon3bii ⊢ ( ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ≠ ∅ ↔ ( dom 𝑓 ∩ ( 𝑔 ‘ 𝑥 ) ) ≠ ∅ )
24 21 23 sylibr ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ≠ ∅ )
25 8 24 jca ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ⊆ 𝑌 ∧ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ≠ ∅ ) )
26 25 ralrimiva ⊢ ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ⊆ 𝑌 ∧ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ≠ ∅ ) )
27 acni2 ⊢ ( ( 𝑌 ∈ AC 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ⊆ 𝑌 ∧ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ≠ ∅ ) ) → ∃ 𝑘 ( 𝑘 : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) )
28 2 26 27 syl2anc ⊢ ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∃ 𝑘 ( 𝑘 : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) )
29 acnrcl ⊢ ( 𝑌 ∈ AC 𝐴 → 𝐴 ∈ V )
30 29 ad3antlr ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( 𝑘 : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → 𝐴 ∈ V )
31 simp-4l ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → 𝑓 : 𝑋 –1-1→ 𝑌 )
32 f1f1orn ⊢ ( 𝑓 : 𝑋 –1-1→ 𝑌 → 𝑓 : 𝑋 –1-1-onto→ ran 𝑓 )
33 31 32 syl ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → 𝑓 : 𝑋 –1-1-onto→ ran 𝑓 )
34 simprr ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) )
35 3 34 sselid ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ( 𝑘 ‘ 𝑥 ) ∈ ran 𝑓 )
36 f1ocnvfv2 ⊢ ( ( 𝑓 : 𝑋 –1-1-onto→ ran 𝑓 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ran 𝑓 ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ) = ( 𝑘 ‘ 𝑥 ) )
37 33 35 36 syl2anc ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ) = ( 𝑘 ‘ 𝑥 ) )
38 37 34 eqeltrd ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) )
39 f1ocnv ⊢ ( 𝑓 : 𝑋 –1-1-onto→ ran 𝑓 → ◡ 𝑓 : ran 𝑓 –1-1-onto→ 𝑋 )
40 f1of ⊢ ( ◡ 𝑓 : ran 𝑓 –1-1-onto→ 𝑋 → ◡ 𝑓 : ran 𝑓 ⟶ 𝑋 )
41 33 39 40 3syl ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ◡ 𝑓 : ran 𝑓 ⟶ 𝑋 )
42 41 35 ffvelcdmd ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ 𝑋 )
43 13 ad2ant2r ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ( 𝑔 ‘ 𝑥 ) ⊆ 𝑋 )
44 f1elima ⊢ ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ 𝑋 ∧ ( 𝑔 ‘ 𝑥 ) ⊆ 𝑋 ) → ( ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ↔ ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ ( 𝑔 ‘ 𝑥 ) ) )
45 31 42 43 44 syl3anc ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ( ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ↔ ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ ( 𝑔 ‘ 𝑥 ) ) )
46 38 45 mpbid ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ ( 𝑔 ‘ 𝑥 ) )
47 46 expr ⊢ ( ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) → ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ ( 𝑔 ‘ 𝑥 ) ) )
48 47 ralimdva ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐴 ⟶ 𝑌 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ ( 𝑔 ‘ 𝑥 ) ) )
49 48 impr ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( 𝑘 : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝐴 ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ ( 𝑔 ‘ 𝑥 ) )
50 acnlem ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ( ◡ 𝑓 ‘ ( 𝑘 ‘ 𝑥 ) ) ∈ ( 𝑔 ‘ 𝑥 ) ) → ∃ ℎ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ 𝑥 ) ∈ ( 𝑔 ‘ 𝑥 ) )
51 30 49 50 syl2anc ⊢ ( ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( 𝑘 : 𝐴 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ‘ 𝑥 ) ∈ ( 𝑓 “ ( 𝑔 ‘ 𝑥 ) ) ) ) → ∃ ℎ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ 𝑥 ) ∈ ( 𝑔 ‘ 𝑥 ) )
52 28 51 exlimddv ⊢ ( ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∃ ℎ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ 𝑥 ) ∈ ( 𝑔 ‘ 𝑥 ) )
53 52 ralrimiva ⊢ ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) → ∀ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ ℎ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ 𝑥 ) ∈ ( 𝑔 ‘ 𝑥 ) )
54 vex ⊢ 𝑓 ∈ V
55 54 dmex ⊢ dom 𝑓 ∈ V
56 14 55 eqeltrrdi ⊢ ( 𝑓 : 𝑋 –1-1→ 𝑌 → 𝑋 ∈ V )
57 isacn ⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑋 ∈ AC 𝐴 ↔ ∀ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ ℎ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ 𝑥 ) ∈ ( 𝑔 ‘ 𝑥 ) ) )
58 56 29 57 syl2an ⊢ ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) → ( 𝑋 ∈ AC 𝐴 ↔ ∀ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ ℎ ∀ 𝑥 ∈ 𝐴 ( ℎ ‘ 𝑥 ) ∈ ( 𝑔 ‘ 𝑥 ) ) )
59 53 58 mpbird ⊢ ( ( 𝑓 : 𝑋 –1-1→ 𝑌 ∧ 𝑌 ∈ AC 𝐴 ) → 𝑋 ∈ AC 𝐴 )
60 59 ex ⊢ ( 𝑓 : 𝑋 –1-1→ 𝑌 → ( 𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴 ) )
61 60 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝑋 –1-1→ 𝑌 → ( 𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴 ) )
62 1 61 syl ⊢ ( 𝑋 ≼ 𝑌 → ( 𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴 ) )