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

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 imbitrrid ⊢ ( 𝑧 ∈ 𝑥 → ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → ( ( 𝑢 ∈ 𝑥 ↦ ∪ { 𝑤 ∈ 𝑢 ∣ ∃ 𝑣 ∈ 𝑦 ( 𝑢 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) } ) ‘ 𝑧 ) ∈ 𝑧 ) )
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 )