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

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 biimtrid ⊢ ( 𝑧 ∈ 𝐴 → ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ≠ ∅ → ∃ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
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 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )