Metamath Proof Explorer


Theorem dfac3

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as the Axiom of Choice (first form) of Enderton p. 49. The right-hand side is the Axiom of Choice of TakeutiZaring p. 83. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004) (Revised by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion dfac3 ( CHOICE ↔ ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 df-ac ( CHOICE ↔ ∀ 𝑦𝑓 ( 𝑓𝑦𝑓 Fn dom 𝑦 ) )
2 vex 𝑥 ∈ V
3 vuniex 𝑥 ∈ V
4 2 3 xpex ( 𝑥 × 𝑥 ) ∈ V
5 simpl ( ( 𝑤𝑥𝑣𝑤 ) → 𝑤𝑥 )
6 elunii ( ( 𝑣𝑤𝑤𝑥 ) → 𝑣 𝑥 )
7 6 ancoms ( ( 𝑤𝑥𝑣𝑤 ) → 𝑣 𝑥 )
8 5 7 jca ( ( 𝑤𝑥𝑣𝑤 ) → ( 𝑤𝑥𝑣 𝑥 ) )
9 8 ssopab2i { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣 𝑥 ) }
10 df-xp ( 𝑥 × 𝑥 ) = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣 𝑥 ) }
11 9 10 sseqtrri { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ⊆ ( 𝑥 × 𝑥 )
12 4 11 ssexi { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∈ V
13 sseq2 ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → ( 𝑓𝑦𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) )
14 dmeq ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → dom 𝑦 = dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } )
15 14 fneq2d ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → ( 𝑓 Fn dom 𝑦𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) )
16 13 15 anbi12d ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → ( ( 𝑓𝑦𝑓 Fn dom 𝑦 ) ↔ ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) ) )
17 16 exbidv ( 𝑦 = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → ( ∃ 𝑓 ( 𝑓𝑦𝑓 Fn dom 𝑦 ) ↔ ∃ 𝑓 ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) ) )
18 12 17 spcv ( ∀ 𝑦𝑓 ( 𝑓𝑦𝑓 Fn dom 𝑦 ) → ∃ 𝑓 ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) )
19 fndm ( 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → dom 𝑓 = dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } )
20 dmopab dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } = { 𝑤 ∣ ∃ 𝑣 ( 𝑤𝑥𝑣𝑤 ) }
21 20 eleq2i ( 𝑧 ∈ dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ↔ 𝑧 ∈ { 𝑤 ∣ ∃ 𝑣 ( 𝑤𝑥𝑣𝑤 ) } )
22 vex 𝑧 ∈ V
23 elequ1 ( 𝑤 = 𝑧 → ( 𝑤𝑥𝑧𝑥 ) )
24 eleq2 ( 𝑤 = 𝑧 → ( 𝑣𝑤𝑣𝑧 ) )
25 23 24 anbi12d ( 𝑤 = 𝑧 → ( ( 𝑤𝑥𝑣𝑤 ) ↔ ( 𝑧𝑥𝑣𝑧 ) ) )
26 25 exbidv ( 𝑤 = 𝑧 → ( ∃ 𝑣 ( 𝑤𝑥𝑣𝑤 ) ↔ ∃ 𝑣 ( 𝑧𝑥𝑣𝑧 ) ) )
27 22 26 elab ( 𝑧 ∈ { 𝑤 ∣ ∃ 𝑣 ( 𝑤𝑥𝑣𝑤 ) } ↔ ∃ 𝑣 ( 𝑧𝑥𝑣𝑧 ) )
28 19.42v ( ∃ 𝑣 ( 𝑧𝑥𝑣𝑧 ) ↔ ( 𝑧𝑥 ∧ ∃ 𝑣 𝑣𝑧 ) )
29 n0 ( 𝑧 ≠ ∅ ↔ ∃ 𝑣 𝑣𝑧 )
30 29 anbi2i ( ( 𝑧𝑥𝑧 ≠ ∅ ) ↔ ( 𝑧𝑥 ∧ ∃ 𝑣 𝑣𝑧 ) )
31 28 30 bitr4i ( ∃ 𝑣 ( 𝑧𝑥𝑣𝑧 ) ↔ ( 𝑧𝑥𝑧 ≠ ∅ ) )
32 21 27 31 3bitrri ( ( 𝑧𝑥𝑧 ≠ ∅ ) ↔ 𝑧 ∈ dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } )
33 eleq2 ( dom 𝑓 = dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → ( 𝑧 ∈ dom 𝑓𝑧 ∈ dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) )
34 32 33 bitr4id ( dom 𝑓 = dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → ( ( 𝑧𝑥𝑧 ≠ ∅ ) ↔ 𝑧 ∈ dom 𝑓 ) )
35 19 34 syl ( 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → ( ( 𝑧𝑥𝑧 ≠ ∅ ) ↔ 𝑧 ∈ dom 𝑓 ) )
36 35 adantl ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) → ( ( 𝑧𝑥𝑧 ≠ ∅ ) ↔ 𝑧 ∈ dom 𝑓 ) )
37 fnfun ( 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } → Fun 𝑓 )
38 funfvima3 ( ( Fun 𝑓𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) → ( 𝑧 ∈ dom 𝑓 → ( 𝑓𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) ) )
39 38 ancoms ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ Fun 𝑓 ) → ( 𝑧 ∈ dom 𝑓 → ( 𝑓𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) ) )
40 37 39 sylan2 ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) → ( 𝑧 ∈ dom 𝑓 → ( 𝑓𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) ) )
41 36 40 sylbid ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ( 𝑓𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) ) )
42 41 imp ( ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) ∧ ( 𝑧𝑥𝑧 ≠ ∅ ) ) → ( 𝑓𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) )
43 imasng ( 𝑧 ∈ V → ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) = { 𝑢𝑧 { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } 𝑢 } )
44 43 elv ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) = { 𝑢𝑧 { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } 𝑢 }
45 vex 𝑢 ∈ V
46 elequ1 ( 𝑣 = 𝑢 → ( 𝑣𝑧𝑢𝑧 ) )
47 46 anbi2d ( 𝑣 = 𝑢 → ( ( 𝑧𝑥𝑣𝑧 ) ↔ ( 𝑧𝑥𝑢𝑧 ) ) )
48 eqid { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } = { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) }
49 22 45 25 47 48 brab ( 𝑧 { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } 𝑢 ↔ ( 𝑧𝑥𝑢𝑧 ) )
50 49 abbii { 𝑢𝑧 { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } 𝑢 } = { 𝑢 ∣ ( 𝑧𝑥𝑢𝑧 ) }
51 44 50 eqtri ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) = { 𝑢 ∣ ( 𝑧𝑥𝑢𝑧 ) }
52 ibar ( 𝑧𝑥 → ( 𝑢𝑧 ↔ ( 𝑧𝑥𝑢𝑧 ) ) )
53 52 abbi2dv ( 𝑧𝑥𝑧 = { 𝑢 ∣ ( 𝑧𝑥𝑢𝑧 ) } )
54 51 53 eqtr4id ( 𝑧𝑥 → ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) = 𝑧 )
55 54 eleq2d ( 𝑧𝑥 → ( ( 𝑓𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) ↔ ( 𝑓𝑧 ) ∈ 𝑧 ) )
56 55 ad2antrl ( ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) ∧ ( 𝑧𝑥𝑧 ≠ ∅ ) ) → ( ( 𝑓𝑧 ) ∈ ( { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } “ { 𝑧 } ) ↔ ( 𝑓𝑧 ) ∈ 𝑧 ) )
57 42 56 mpbid ( ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) ∧ ( 𝑧𝑥𝑧 ≠ ∅ ) ) → ( 𝑓𝑧 ) ∈ 𝑧 )
58 57 exp32 ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) → ( 𝑧𝑥 → ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) ) )
59 58 ralrimiv ( ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) → ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
60 59 eximi ( ∃ 𝑓 ( 𝑓 ⊆ { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ∧ 𝑓 Fn dom { ⟨ 𝑤 , 𝑣 ⟩ ∣ ( 𝑤𝑥𝑣𝑤 ) } ) → ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
61 18 60 syl ( ∀ 𝑦𝑓 ( 𝑓𝑦𝑓 Fn dom 𝑦 ) → ∃ 𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
62 61 alrimiv ( ∀ 𝑦𝑓 ( 𝑓𝑦𝑓 Fn dom 𝑦 ) → ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
63 eqid ( 𝑤 ∈ dom 𝑦 ↦ ( 𝑓 ‘ { 𝑢𝑤 𝑦 𝑢 } ) ) = ( 𝑤 ∈ dom 𝑦 ↦ ( 𝑓 ‘ { 𝑢𝑤 𝑦 𝑢 } ) )
64 63 aceq3lem ( ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ∃ 𝑓 ( 𝑓𝑦𝑓 Fn dom 𝑦 ) )
65 64 alrimiv ( ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) → ∀ 𝑦𝑓 ( 𝑓𝑦𝑓 Fn dom 𝑦 ) )
66 62 65 impbii ( ∀ 𝑦𝑓 ( 𝑓𝑦𝑓 Fn dom 𝑦 ) ↔ ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )
67 1 66 bitri ( CHOICE ↔ ∀ 𝑥𝑓𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑓𝑧 ) ∈ 𝑧 ) )