Metamath Proof Explorer

Theorem dfac9

Description: Equivalence of the axiom of choice with a statement related to ac9 ; definition AC3 of Schechter p. 139. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion dfac9 ( CHOICE ↔ ∀ 𝑓 ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 dfac3 ⊢ ( CHOICE ↔ ∀ 𝑠 ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
2 vex ⊢ 𝑓 ∈ V
3 2 rnex ⊢ ran 𝑓 ∈ V
4 raleq ⊢ ( 𝑠 = ran 𝑓 → ( ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ↔ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) )
5 4 exbidv ⊢ ( 𝑠 = ran 𝑓 → ( ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ↔ ∃ 𝑔 ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) )
6 3 5 spcv ⊢ ( ∀ 𝑠 ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) → ∃ 𝑔 ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
7 df-nel ⊢ ( ∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ran 𝑓 )
8 7 biimpi ⊢ ( ∅ ∉ ran 𝑓 → ¬ ∅ ∈ ran 𝑓 )
9 8 ad2antlr ⊢ ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ 𝑥 ∈ dom 𝑓 ) → ¬ ∅ ∈ ran 𝑓 )
10 fvelrn ⊢ ( ( Fun 𝑓 ∧ 𝑥 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
11 10 adantlr ⊢ ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ 𝑥 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
12 eleq1 ⊢ ( ( 𝑓 ‘ 𝑥 ) = ∅ → ( ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓 ) )
13 11 12 syl5ibcom ⊢ ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ 𝑥 ∈ dom 𝑓 ) → ( ( 𝑓 ‘ 𝑥 ) = ∅ → ∅ ∈ ran 𝑓 ) )
14 13 necon3bd ⊢ ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ 𝑥 ∈ dom 𝑓 ) → ( ¬ ∅ ∈ ran 𝑓 → ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )
15 9 14 mpd ⊢ ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ 𝑥 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑥 ) ≠ ∅ )
16 15 adantlr ⊢ ( ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) ∧ 𝑥 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑥 ) ≠ ∅ )
17 neeq1 ⊢ ( 𝑡 = ( 𝑓 ‘ 𝑥 ) → ( 𝑡 ≠ ∅ ↔ ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )
18 fveq2 ⊢ ( 𝑡 = ( 𝑓 ‘ 𝑥 ) → ( 𝑔 ‘ 𝑡 ) = ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) )
19 id ⊢ ( 𝑡 = ( 𝑓 ‘ 𝑥 ) → 𝑡 = ( 𝑓 ‘ 𝑥 ) )
20 18 19 eleq12d ⊢ ( 𝑡 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ↔ ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
21 17 20 imbi12d ⊢ ( 𝑡 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ↔ ( ( 𝑓 ‘ 𝑥 ) ≠ ∅ → ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) ) ) )
22 simplr ⊢ ( ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) ∧ 𝑥 ∈ dom 𝑓 ) → ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
23 10 ad4ant14 ⊢ ( ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) ∧ 𝑥 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
24 21 22 23 rspcdva ⊢ ( ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) ∧ 𝑥 ∈ dom 𝑓 ) → ( ( 𝑓 ‘ 𝑥 ) ≠ ∅ → ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
25 16 24 mpd ⊢ ( ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) ∧ 𝑥 ∈ dom 𝑓 ) → ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) )
26 25 ralrimiva ⊢ ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) → ∀ 𝑥 ∈ dom 𝑓 ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) )
27 2 dmex ⊢ dom 𝑓 ∈ V
28 mptelixpg ⊢ ( dom 𝑓 ∈ V → ( ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ dom 𝑓 ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
29 27 28 ax-mp ⊢ ( ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ dom 𝑓 ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ∈ ( 𝑓 ‘ 𝑥 ) )
30 26 29 sylibr ⊢ ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) → ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑔 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) )
31 30 ne0d ⊢ ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ∧ ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ )
32 31 ex ⊢ ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → ( ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )
33 32 exlimdv ⊢ ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → ( ∃ 𝑔 ∀ 𝑡 ∈ ran 𝑓 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )
34 6 33 syl5com ⊢ ( ∀ 𝑠 ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) → ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )
35 34 alrimiv ⊢ ( ∀ 𝑠 ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) → ∀ 𝑓 ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )
36 fnresi ⊢ ( I ↾ ( 𝑠 ∖ { ∅ } ) ) Fn ( 𝑠 ∖ { ∅ } )
37 fnfun ⊢ ( ( I ↾ ( 𝑠 ∖ { ∅ } ) ) Fn ( 𝑠 ∖ { ∅ } ) → Fun ( I ↾ ( 𝑠 ∖ { ∅ } ) ) )
38 36 37 ax-mp ⊢ Fun ( I ↾ ( 𝑠 ∖ { ∅ } ) )
39 neldifsn ⊢ ¬ ∅ ∈ ( 𝑠 ∖ { ∅ } )
40 vex ⊢ 𝑠 ∈ V
41 40 difexi ⊢ ( 𝑠 ∖ { ∅ } ) ∈ V
42 resiexg ⊢ ( ( 𝑠 ∖ { ∅ } ) ∈ V → ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ∈ V )
43 41 42 ax-mp ⊢ ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ∈ V
44 funeq ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ( Fun 𝑓 ↔ Fun ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ) )
45 rneq ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ran 𝑓 = ran ( I ↾ ( 𝑠 ∖ { ∅ } ) ) )
46 rnresi ⊢ ran ( I ↾ ( 𝑠 ∖ { ∅ } ) ) = ( 𝑠 ∖ { ∅ } )
47 45 46 eqtrdi ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ran 𝑓 = ( 𝑠 ∖ { ∅ } ) )
48 47 eleq2d ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ( ∅ ∈ ran 𝑓 ↔ ∅ ∈ ( 𝑠 ∖ { ∅ } ) ) )
49 48 notbid ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ( ¬ ∅ ∈ ran 𝑓 ↔ ¬ ∅ ∈ ( 𝑠 ∖ { ∅ } ) ) )
50 7 49 syl5bb ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ( ∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ( 𝑠 ∖ { ∅ } ) ) )
51 44 50 anbi12d ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) ↔ ( Fun ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ∧ ¬ ∅ ∈ ( 𝑠 ∖ { ∅ } ) ) ) )
52 dmeq ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → dom 𝑓 = dom ( I ↾ ( 𝑠 ∖ { ∅ } ) ) )
53 dmresi ⊢ dom ( I ↾ ( 𝑠 ∖ { ∅ } ) ) = ( 𝑠 ∖ { ∅ } )
54 52 53 eqtrdi ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → dom 𝑓 = ( 𝑠 ∖ { ∅ } ) )
55 54 ixpeq1d ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) = X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) ( 𝑓 ‘ 𝑥 ) )
56 fveq1 ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ‘ 𝑥 ) )
57 fvresi ⊢ ( 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) → ( ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ‘ 𝑥 ) = 𝑥 )
58 56 57 sylan9eq ⊢ ( ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ∧ 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 )
59 58 ixpeq2dva ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) ( 𝑓 ‘ 𝑥 ) = X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 )
60 55 59 eqtrd ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) = X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 )
61 60 neeq1d ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ( X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ↔ X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 ≠ ∅ ) )
62 51 61 imbi12d ⊢ ( 𝑓 = ( I ↾ ( 𝑠 ∖ { ∅ } ) ) → ( ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) ↔ ( ( Fun ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ∧ ¬ ∅ ∈ ( 𝑠 ∖ { ∅ } ) ) → X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 ≠ ∅ ) ) )
63 43 62 spcv ⊢ ( ∀ 𝑓 ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) → ( ( Fun ( I ↾ ( 𝑠 ∖ { ∅ } ) ) ∧ ¬ ∅ ∈ ( 𝑠 ∖ { ∅ } ) ) → X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 ≠ ∅ ) )
64 38 39 63 mp2ani ⊢ ( ∀ 𝑓 ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) → X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 ≠ ∅ )
65 n0 ⊢ ( X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 )
66 vex ⊢ 𝑔 ∈ V
67 66 elixp ⊢ ( 𝑔 ∈ X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 ↔ ( 𝑔 Fn ( 𝑠 ∖ { ∅ } ) ∧ ∀ 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) )
68 eldifsn ⊢ ( 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) ↔ ( 𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅ ) )
69 68 imbi1i ⊢ ( ( 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ( ( 𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅ ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) )
70 impexp ⊢ ( ( ( 𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅ ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑠 → ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) )
71 69 70 bitri ⊢ ( ( 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝑠 → ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) )
72 71 ralbii2 ⊢ ( ∀ 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝑠 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) )
73 neeq1 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅ ) )
74 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑡 ) )
75 id ⊢ ( 𝑥 = 𝑡 → 𝑥 = 𝑡 )
76 74 75 eleq12d ⊢ ( 𝑥 = 𝑡 → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ↔ ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
77 73 76 imbi12d ⊢ ( 𝑥 = 𝑡 → ( ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ) )
78 77 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑠 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
79 72 78 bitri ⊢ ( ∀ 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ↔ ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
80 79 biimpi ⊢ ( ∀ 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 → ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
81 67 80 simplbiim ⊢ ( 𝑔 ∈ X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 → ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
82 81 eximi ⊢ ( ∃ 𝑔 𝑔 ∈ X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 → ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
83 65 82 sylbi ⊢ ( X 𝑥 ∈ ( 𝑠 ∖ { ∅ } ) 𝑥 ≠ ∅ → ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
84 64 83 syl ⊢ ( ∀ 𝑓 ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) → ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
85 84 alrimiv ⊢ ( ∀ 𝑓 ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) → ∀ 𝑠 ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) )
86 35 85 impbii ⊢ ( ∀ 𝑠 ∃ 𝑔 ∀ 𝑡 ∈ 𝑠 ( 𝑡 ≠ ∅ → ( 𝑔 ‘ 𝑡 ) ∈ 𝑡 ) ↔ ∀ 𝑓 ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )
87 1 86 bitri ⊢ ( CHOICE ↔ ∀ 𝑓 ( ( Fun 𝑓 ∧ ∅ ∉ ran 𝑓 ) → X 𝑥 ∈ dom 𝑓 ( 𝑓 ‘ 𝑥 ) ≠ ∅ ) )