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 ⊢ A ∈ V
ac6c4.2 ⊢ B ∈ V
Assertion ac6c4 ⊢ ∀ x ∈ A B ≠ ∅ → ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 ac6c4.1 ⊢ A ∈ V
2 ac6c4.2 ⊢ B ∈ V
3 nfv ⊢ Ⅎ z B ≠ ∅
4 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ B
5 nfcv ⊢ Ⅎ _ x ∅
6 4 5 nfne ⊢ Ⅎ x ⦋ z / x⦌ B ≠ ∅
7 csbeq1a ⊢ x = z → B = ⦋ z / x⦌ B
8 7 neeq1d ⊢ x = z → B ≠ ∅ ↔ ⦋ z / x⦌ B ≠ ∅
9 3 6 8 cbvralw ⊢ ∀ x ∈ A B ≠ ∅ ↔ ∀ z ∈ A ⦋ z / x⦌ B ≠ ∅
10 n0 ⊢ ⦋ z / x⦌ B ≠ ∅ ↔ ∃ y y ∈ ⦋ z / x⦌ B
11 nfv ⊢ Ⅎ y z ∈ A
12 nfre1 ⊢ Ⅎ y ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B
13 4 nfel2 ⊢ Ⅎ x y ∈ ⦋ z / x⦌ B
14 7 eleq2d ⊢ x = z → y ∈ B ↔ y ∈ ⦋ z / x⦌ B
15 13 14 rspce ⊢ z ∈ A ∧ y ∈ ⦋ z / x⦌ B → ∃ x ∈ A y ∈ B
16 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
17 15 16 sylibr ⊢ z ∈ A ∧ y ∈ ⦋ z / x⦌ B → y ∈ ⋃ x ∈ A B
18 rspe ⊢ y ∈ ⋃ x ∈ A B ∧ y ∈ ⦋ z / x⦌ B → ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B
19 17 18 sylancom ⊢ z ∈ A ∧ y ∈ ⦋ z / x⦌ B → ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B
20 19 ex ⊢ z ∈ A → y ∈ ⦋ z / x⦌ B → ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B
21 11 12 20 exlimd ⊢ z ∈ A → ∃ y y ∈ ⦋ z / x⦌ B → ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B
22 10 21 biimtrid ⊢ z ∈ A → ⦋ z / x⦌ B ≠ ∅ → ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B
23 22 ralimia ⊢ ∀ z ∈ A ⦋ z / x⦌ B ≠ ∅ → ∀ z ∈ A ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B
24 9 23 sylbi ⊢ ∀ x ∈ A B ≠ ∅ → ∀ z ∈ A ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B
25 1 2 iunex ⊢ ⋃ x ∈ A B ∈ V
26 eleq1 ⊢ y = f ⁡ z → y ∈ ⦋ z / x⦌ B ↔ f ⁡ z ∈ ⦋ z / x⦌ B
27 1 25 26 ac6 ⊢ ∀ z ∈ A ∃ y ∈ ⋃ x ∈ A B y ∈ ⦋ z / x⦌ B → ∃ f f : A ⟶ ⋃ x ∈ A B ∧ ∀ z ∈ A f ⁡ z ∈ ⦋ z / x⦌ B
28 ffn ⊢ f : A ⟶ ⋃ x ∈ A B → f Fn A
29 nfv ⊢ Ⅎ z f ⁡ x ∈ B
30 4 nfel2 ⊢ Ⅎ x f ⁡ z ∈ ⦋ z / x⦌ B
31 fveq2 ⊢ x = z → f ⁡ x = f ⁡ z
32 31 7 eleq12d ⊢ x = z → f ⁡ x ∈ B ↔ f ⁡ z ∈ ⦋ z / x⦌ B
33 29 30 32 cbvralw ⊢ ∀ x ∈ A f ⁡ x ∈ B ↔ ∀ z ∈ A f ⁡ z ∈ ⦋ z / x⦌ B
34 33 biimpri ⊢ ∀ z ∈ A f ⁡ z ∈ ⦋ z / x⦌ B → ∀ x ∈ A f ⁡ x ∈ B
35 28 34 anim12i ⊢ f : A ⟶ ⋃ x ∈ A B ∧ ∀ z ∈ A f ⁡ z ∈ ⦋ z / x⦌ B → f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
36 35 eximi ⊢ ∃ f f : A ⟶ ⋃ x ∈ A B ∧ ∀ z ∈ A f ⁡ z ∈ ⦋ z / x⦌ B → ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
37 24 27 36 3syl ⊢ ∀ x ∈ A B ≠ ∅ → ∃ f f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B