Metamath Proof Explorer


Theorem dfac2a

Description: Our Axiom of Choice (in the form of ac3 ) implies the Axiom of Choice (first form) of Enderton p. 49. The proof uses neither AC nor the Axiom of Regularity. See dfac2b for the converse (which does use the Axiom of Regularity). (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion dfac2a ( ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) → CHOICE )

Proof

Step Hyp Ref Expression
1 riotauni ( ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) → ( 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) = { 𝑤𝑧 ∣ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) } )
2 riotacl ( ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) → ( 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) ∈ 𝑧 )
3 1 2 eqeltrrd ( ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) → { 𝑤𝑧 ∣ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) } ∈ 𝑧 )
4 elequ2 ( 𝑢 = 𝑧 → ( 𝑤𝑢𝑤𝑧 ) )
5 elequ1 ( 𝑢 = 𝑧 → ( 𝑢𝑣𝑧𝑣 ) )
6 5 anbi1d ( 𝑢 = 𝑧 → ( ( 𝑢𝑣𝑤𝑣 ) ↔ ( 𝑧𝑣𝑤𝑣 ) ) )
7 6 rexbidv ( 𝑢 = 𝑧 → ( ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) ↔ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
8 4 7 anbi12d ( 𝑢 = 𝑧 → ( ( 𝑤𝑢 ∧ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) ) ↔ ( 𝑤𝑧 ∧ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) ) )
9 8 rabbidva2 ( 𝑢 = 𝑧 → { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } = { 𝑤𝑧 ∣ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) } )
10 9 unieqd ( 𝑢 = 𝑧 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } = { 𝑤𝑧 ∣ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) } )
11 eqid ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) = ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } )
12 vex 𝑧 ∈ V
13 12 rabex { 𝑤𝑧 ∣ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) } ∈ V
14 13 uniex { 𝑤𝑧 ∣ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) } ∈ V
15 10 11 14 fvmpt ( 𝑧𝑥 → ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) = { 𝑤𝑧 ∣ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) } )
16 15 eleq1d ( 𝑧𝑥 → ( ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 { 𝑤𝑧 ∣ ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) } ∈ 𝑧 ) )
17 3 16 syl5ibr ( 𝑧𝑥 → ( ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) → ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) )
18 17 imim2d ( 𝑧𝑥 → ( ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) → ( 𝑧 ≠ ∅ → ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
19 18 ralimia ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) → ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) )
20 ssrab2 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ⊆ 𝑢
21 elssuni ( 𝑢𝑥𝑢 𝑥 )
22 20 21 sstrid ( 𝑢𝑥 → { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ⊆ 𝑥 )
23 22 unissd ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ⊆ 𝑥 )
24 vex 𝑥 ∈ V
25 24 uniex 𝑥 ∈ V
26 25 uniex 𝑥 ∈ V
27 26 elpw2 ( { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ∈ 𝒫 𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ⊆ 𝑥 )
28 23 27 sylibr ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ∈ 𝒫 𝑥 )
29 11 28 fmpti ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) : 𝑥 ⟶ 𝒫 𝑥
30 26 pwex 𝒫 𝑥 ∈ V
31 fex2 ( ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) : 𝑥 ⟶ 𝒫 𝑥𝑥 ∈ V ∧ 𝒫 𝑥 ∈ V ) → ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ∈ V )
32 29 24 30 31 mp3an ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ∈ V
33 fveq1 ( 𝑓 = ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) → ( 𝑓𝑧 ) = ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) )
34 33 eleq1d ( 𝑓 = ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) → ( ( 𝑓𝑧 ) ∈ 𝑧 ↔ ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) )
35 34 imbi2d ( 𝑓 = ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) → ( ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
36 35 ralbidv ( 𝑓 = ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) → ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) ) )
37 32 36 spcev ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( ( 𝑢𝑥 { 𝑤𝑢 ∣ ∃ 𝑣𝑦 ( 𝑢𝑣𝑤𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
38 19 37 syl ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) → ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
39 38 exlimiv ( ∃ 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) → ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
40 39 alimi ( ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) → ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
41 dfac3 ( CHOICE ↔ ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
42 40 41 sylibr ( ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) → CHOICE )