Metamath Proof Explorer

Theorem acndom

Description: A set with long choice sequences also has shorter choice sequences, where "shorter" here means the new index set is dominated by the old index set. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acndom ( 𝐴 ≼ 𝐵 → ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴 ) )

Proof

Step Hyp Ref Expression
1 brdomi ⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
2 neq0 ⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
3 simpl3 ⊢ ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → 𝑋 ∈ AC 𝐵 )
4 elmapi ⊢ ( 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) → 𝑔 : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) )
5 4 ad2antlr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑔 : 𝐴 ⟶ ( 𝒫 𝑋 ∖ { ∅ } ) )
6 simpll1 ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
7 f1f1orn ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 )
8 f1ocnv ⊢ ( 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 → ◡ 𝑓 : ran 𝑓 –1-1-onto→ 𝐴 )
9 f1of ⊢ ( ◡ 𝑓 : ran 𝑓 –1-1-onto→ 𝐴 → ◡ 𝑓 : ran 𝑓 ⟶ 𝐴 )
10 6 7 8 9 4syl ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → ◡ 𝑓 : ran 𝑓 ⟶ 𝐴 )
11 10 ffvelrnda ⊢ ( ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ran 𝑓 ) → ( ◡ 𝑓 ‘ 𝑦 ) ∈ 𝐴 )
12 simpl2 ⊢ ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → 𝑥 ∈ 𝐴 )
13 12 ad2antrr ⊢ ( ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ¬ 𝑦 ∈ ran 𝑓 ) → 𝑥 ∈ 𝐴 )
14 11 13 ifclda ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ∈ 𝐴 )
15 5 14 ffvelrnd ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ∈ ( 𝒫 𝑋 ∖ { ∅ } ) )
16 eldifsn ⊢ ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ∈ ( 𝒫 𝑋 ∖ { ∅ } ) ↔ ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ∈ 𝒫 𝑋 ∧ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ≠ ∅ ) )
17 elpwi ⊢ ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ∈ 𝒫 𝑋 → ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ⊆ 𝑋 )
18 17 anim1i ⊢ ( ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ∈ 𝒫 𝑋 ∧ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ≠ ∅ ) → ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ⊆ 𝑋 ∧ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ≠ ∅ ) )
19 16 18 sylbi ⊢ ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ∈ ( 𝒫 𝑋 ∖ { ∅ } ) → ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ⊆ 𝑋 ∧ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ≠ ∅ ) )
20 15 19 syl ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ⊆ 𝑋 ∧ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ≠ ∅ ) )
21 20 ralrimiva ⊢ ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∀ 𝑦 ∈ 𝐵 ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ⊆ 𝑋 ∧ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ≠ ∅ ) )
22 acni2 ⊢ ( ( 𝑋 ∈ AC 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ⊆ 𝑋 ∧ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ≠ ∅ ) ) → ∃ 𝑘 ( 𝑘 : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ) )
23 3 21 22 syl2anc ⊢ ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∃ 𝑘 ( 𝑘 : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ) )
24 f1dm ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → dom 𝑓 = 𝐴 )
25 vex ⊢ 𝑓 ∈ V
26 25 dmex ⊢ dom 𝑓 ∈ V
27 24 26 eqeltrrdi ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝐴 ∈ V )
28 27 3ad2ant1 ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) → 𝐴 ∈ V )
29 28 ad2antrr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( 𝑘 : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ) ) → 𝐴 ∈ V )
30 simpll1 ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
31 f1f ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
32 frn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ran 𝑓 ⊆ 𝐵 )
33 ssralv ⊢ ( ran 𝑓 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) → ∀ 𝑦 ∈ ran 𝑓 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ) )
34 30 31 32 33 4syl ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) → ∀ 𝑦 ∈ ran 𝑓 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ) )
35 iftrue ⊢ ( 𝑦 ∈ ran 𝑓 → if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) = ( ◡ 𝑓 ‘ 𝑦 ) )
36 35 fveq2d ⊢ ( 𝑦 ∈ ran 𝑓 → ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) = ( 𝑔 ‘ ( ◡ 𝑓 ‘ 𝑦 ) ) )
37 36 eleq2d ⊢ ( 𝑦 ∈ ran 𝑓 → ( ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ↔ ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ 𝑦 ) ) ) )
38 37 ralbiia ⊢ ( ∀ 𝑦 ∈ ran 𝑓 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ↔ ∀ 𝑦 ∈ ran 𝑓 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ 𝑦 ) ) )
39 34 38 syl6ib ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) → ∀ 𝑦 ∈ ran 𝑓 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ 𝑦 ) ) ) )
40 f1fn ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝑓 Fn 𝐴 )
41 fveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( 𝑘 ‘ 𝑦 ) = ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) )
42 2fveq3 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( 𝑔 ‘ ( ◡ 𝑓 ‘ 𝑦 ) ) = ( 𝑔 ‘ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ) )
43 41 42 eleq12d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ) )
44 43 ralrn ⊢ ( 𝑓 Fn 𝐴 → ( ∀ 𝑦 ∈ ran 𝑓 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ) )
45 30 40 44 3syl ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) → ( ∀ 𝑦 ∈ ran 𝑓 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ) )
46 39 45 sylibd ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ) )
47 30 7 syl ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) → 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 )
48 f1ocnvfv1 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 ∧ 𝑧 ∈ 𝐴 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) = 𝑧 )
49 47 48 sylan ⊢ ( ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) ∧ 𝑧 ∈ 𝐴 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) = 𝑧 )
50 49 fveq2d ⊢ ( ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑔 ‘ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ) = ( 𝑔 ‘ 𝑧 ) )
51 50 eleq2d ⊢ ( ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ↔ ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ 𝑧 ) ) )
52 51 ralbidva ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ 𝑧 ) ) )
53 46 52 sylibd ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ 𝑘 : 𝐵 ⟶ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ 𝑧 ) ) )
54 53 impr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( 𝑘 : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ 𝑧 ) )
55 acnlem ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑘 ‘ ( 𝑓 ‘ 𝑧 ) ) ∈ ( 𝑔 ‘ 𝑧 ) ) → ∃ ℎ ∀ 𝑧 ∈ 𝐴 ( ℎ ‘ 𝑧 ) ∈ ( 𝑔 ‘ 𝑧 ) )
56 29 54 55 syl2anc ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) ∧ ( 𝑘 : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑘 ‘ 𝑦 ) ∈ ( 𝑔 ‘ if ( 𝑦 ∈ ran 𝑓 , ( ◡ 𝑓 ‘ 𝑦 ) , 𝑥 ) ) ) ) → ∃ ℎ ∀ 𝑧 ∈ 𝐴 ( ℎ ‘ 𝑧 ) ∈ ( 𝑔 ‘ 𝑧 ) )
57 23 56 exlimddv ⊢ ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) ∧ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∃ ℎ ∀ 𝑧 ∈ 𝐴 ( ℎ ‘ 𝑧 ) ∈ ( 𝑔 ‘ 𝑧 ) )
58 57 ralrimiva ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) → ∀ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ ℎ ∀ 𝑧 ∈ 𝐴 ( ℎ ‘ 𝑧 ) ∈ ( 𝑔 ‘ 𝑧 ) )
59 elex ⊢ ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ V )
60 isacn ⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑋 ∈ AC 𝐴 ↔ ∀ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ ℎ ∀ 𝑧 ∈ 𝐴 ( ℎ ‘ 𝑧 ) ∈ ( 𝑔 ‘ 𝑧 ) ) )
61 59 27 60 syl2anr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑋 ∈ AC 𝐵 ) → ( 𝑋 ∈ AC 𝐴 ↔ ∀ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ ℎ ∀ 𝑧 ∈ 𝐴 ( ℎ ‘ 𝑧 ) ∈ ( 𝑔 ‘ 𝑧 ) ) )
62 61 3adant2 ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) → ( 𝑋 ∈ AC 𝐴 ↔ ∀ 𝑔 ∈ ( ( 𝒫 𝑋 ∖ { ∅ } ) ↑m 𝐴 ) ∃ ℎ ∀ 𝑧 ∈ 𝐴 ( ℎ ‘ 𝑧 ) ∈ ( 𝑔 ‘ 𝑧 ) ) )
63 58 62 mpbird ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑋 ∈ AC 𝐵 ) → 𝑋 ∈ AC 𝐴 )
64 63 3exp ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴 ) ) )
65 64 exlimdv ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴 ) ) )
66 2 65 syl5bi ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ( ¬ 𝐴 = ∅ → ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴 ) ) )
67 acneq ⊢ ( 𝐴 = ∅ → AC 𝐴 = AC ∅ )
68 0fin ⊢ ∅ ∈ Fin
69 finacn ⊢ ( ∅ ∈ Fin → AC ∅ = V )
70 68 69 ax-mp ⊢ AC ∅ = V
71 67 70 eqtrdi ⊢ ( 𝐴 = ∅ → AC 𝐴 = V )
72 71 eleq2d ⊢ ( 𝐴 = ∅ → ( 𝑋 ∈ AC 𝐴 ↔ 𝑋 ∈ V ) )
73 59 72 syl5ibr ⊢ ( 𝐴 = ∅ → ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴 ) )
74 66 73 pm2.61d2 ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴 ) )
75 74 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 → ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴 ) )
76 1 75 syl ⊢ ( 𝐴 ≼ 𝐵 → ( 𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴 ) )