Metamath Proof Explorer


Theorem ac6c4

Description: Equivalent of Axiom of Choice. B is a collection B ( x ) of nonempty sets. (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Hypotheses ac6c4.1 𝐴 ∈ V
ac6c4.2 𝐵 ∈ V
Assertion ac6c4 ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ac6c4.1 𝐴 ∈ V
2 ac6c4.2 𝐵 ∈ V
3 nfv 𝑧 𝐵 ≠ ∅
4 nfcsb1v 𝑥 𝑧 / 𝑥 𝐵
5 nfcv 𝑥
6 4 5 nfne 𝑥 𝑧 / 𝑥 𝐵 ≠ ∅
7 csbeq1a ( 𝑥 = 𝑧𝐵 = 𝑧 / 𝑥 𝐵 )
8 7 neeq1d ( 𝑥 = 𝑧 → ( 𝐵 ≠ ∅ ↔ 𝑧 / 𝑥 𝐵 ≠ ∅ ) )
9 3 6 8 cbvralw ( ∀ 𝑥𝐴 𝐵 ≠ ∅ ↔ ∀ 𝑧𝐴 𝑧 / 𝑥 𝐵 ≠ ∅ )
10 n0 ( 𝑧 / 𝑥 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 𝑧 / 𝑥 𝐵 )
11 nfv 𝑦 𝑧𝐴
12 nfre1 𝑦𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵
13 4 nfel2 𝑥 𝑦 𝑧 / 𝑥 𝐵
14 7 eleq2d ( 𝑥 = 𝑧 → ( 𝑦𝐵𝑦 𝑧 / 𝑥 𝐵 ) )
15 13 14 rspce ( ( 𝑧𝐴𝑦 𝑧 / 𝑥 𝐵 ) → ∃ 𝑥𝐴 𝑦𝐵 )
16 eliun ( 𝑦 𝑥𝐴 𝐵 ↔ ∃ 𝑥𝐴 𝑦𝐵 )
17 15 16 sylibr ( ( 𝑧𝐴𝑦 𝑧 / 𝑥 𝐵 ) → 𝑦 𝑥𝐴 𝐵 )
18 rspe ( ( 𝑦 𝑥𝐴 𝐵𝑦 𝑧 / 𝑥 𝐵 ) → ∃ 𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵 )
19 17 18 sylancom ( ( 𝑧𝐴𝑦 𝑧 / 𝑥 𝐵 ) → ∃ 𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵 )
20 19 ex ( 𝑧𝐴 → ( 𝑦 𝑧 / 𝑥 𝐵 → ∃ 𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵 ) )
21 11 12 20 exlimd ( 𝑧𝐴 → ( ∃ 𝑦 𝑦 𝑧 / 𝑥 𝐵 → ∃ 𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵 ) )
22 10 21 syl5bi ( 𝑧𝐴 → ( 𝑧 / 𝑥 𝐵 ≠ ∅ → ∃ 𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵 ) )
23 22 ralimia ( ∀ 𝑧𝐴 𝑧 / 𝑥 𝐵 ≠ ∅ → ∀ 𝑧𝐴𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵 )
24 9 23 sylbi ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∀ 𝑧𝐴𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵 )
25 1 2 iunex 𝑥𝐴 𝐵 ∈ V
26 eleq1 ( 𝑦 = ( 𝑓𝑧 ) → ( 𝑦 𝑧 / 𝑥 𝐵 ↔ ( 𝑓𝑧 ) ∈ 𝑧 / 𝑥 𝐵 ) )
27 1 25 26 ac6 ( ∀ 𝑧𝐴𝑦 𝑥𝐴 𝐵 𝑦 𝑧 / 𝑥 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐴 𝑥𝐴 𝐵 ∧ ∀ 𝑧𝐴 ( 𝑓𝑧 ) ∈ 𝑧 / 𝑥 𝐵 ) )
28 ffn ( 𝑓 : 𝐴 𝑥𝐴 𝐵𝑓 Fn 𝐴 )
29 nfv 𝑧 ( 𝑓𝑥 ) ∈ 𝐵
30 4 nfel2 𝑥 ( 𝑓𝑧 ) ∈ 𝑧 / 𝑥 𝐵
31 fveq2 ( 𝑥 = 𝑧 → ( 𝑓𝑥 ) = ( 𝑓𝑧 ) )
32 31 7 eleq12d ( 𝑥 = 𝑧 → ( ( 𝑓𝑥 ) ∈ 𝐵 ↔ ( 𝑓𝑧 ) ∈ 𝑧 / 𝑥 𝐵 ) )
33 29 30 32 cbvralw ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ↔ ∀ 𝑧𝐴 ( 𝑓𝑧 ) ∈ 𝑧 / 𝑥 𝐵 )
34 33 biimpri ( ∀ 𝑧𝐴 ( 𝑓𝑧 ) ∈ 𝑧 / 𝑥 𝐵 → ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 )
35 28 34 anim12i ( ( 𝑓 : 𝐴 𝑥𝐴 𝐵 ∧ ∀ 𝑧𝐴 ( 𝑓𝑧 ) ∈ 𝑧 / 𝑥 𝐵 ) → ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
36 35 eximi ( ∃ 𝑓 ( 𝑓 : 𝐴 𝑥𝐴 𝐵 ∧ ∀ 𝑧𝐴 ( 𝑓𝑧 ) ∈ 𝑧 / 𝑥 𝐵 ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
37 24 27 36 3syl ( ∀ 𝑥𝐴 𝐵 ≠ ∅ → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )