Metamath Proof Explorer

Theorem acni2

Description: The property of being a choice set of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acni2 ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ B ∈ 𝒫 X ∖ ∅ ↔ B ∈ 𝒫 X ∧ B ≠ ∅
2 elpw2g ⊢ X ∈ AC _ A → B ∈ 𝒫 X ↔ B ⊆ X
3 2 anbi1d ⊢ X ∈ AC _ A → B ∈ 𝒫 X ∧ B ≠ ∅ ↔ B ⊆ X ∧ B ≠ ∅
4 1 3 bitrid ⊢ X ∈ AC _ A → B ∈ 𝒫 X ∖ ∅ ↔ B ⊆ X ∧ B ≠ ∅
5 4 ralbidv ⊢ X ∈ AC _ A → ∀ x ∈ A B ∈ 𝒫 X ∖ ∅ ↔ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅
6 5 biimpar ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∀ x ∈ A B ∈ 𝒫 X ∖ ∅
7 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
8 7 fmpt ⊢ ∀ x ∈ A B ∈ 𝒫 X ∖ ∅ ↔ x ∈ A ⟼ B : A ⟶ 𝒫 X ∖ ∅
9 6 8 sylib ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → x ∈ A ⟼ B : A ⟶ 𝒫 X ∖ ∅
10 acni ⊢ X ∈ AC _ A ∧ x ∈ A ⟼ B : A ⟶ 𝒫 X ∖ ∅ → ∃ f ∀ y ∈ A f ⁡ y ∈ x ∈ A ⟼ B ⁡ y
11 9 10 syldan ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∃ f ∀ y ∈ A f ⁡ y ∈ x ∈ A ⟼ B ⁡ y
12 nffvmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B ⁡ y
13 12 nfel2 ⊢ Ⅎ x f ⁡ y ∈ x ∈ A ⟼ B ⁡ y
14 nfv ⊢ Ⅎ y f ⁡ x ∈ x ∈ A ⟼ B ⁡ x
15 fveq2 ⊢ y = x → f ⁡ y = f ⁡ x
16 fveq2 ⊢ y = x → x ∈ A ⟼ B ⁡ y = x ∈ A ⟼ B ⁡ x
17 15 16 eleq12d ⊢ y = x → f ⁡ y ∈ x ∈ A ⟼ B ⁡ y ↔ f ⁡ x ∈ x ∈ A ⟼ B ⁡ x
18 13 14 17 cbvralw ⊢ ∀ y ∈ A f ⁡ y ∈ x ∈ A ⟼ B ⁡ y ↔ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x
19 simplr ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → ∀ x ∈ A B ⊆ X ∧ B ≠ ∅
20 simplr ⊢ X ∈ AC _ A ∧ x ∈ A ∧ B ⊆ X → x ∈ A
21 simpll ⊢ X ∈ AC _ A ∧ x ∈ A ∧ B ⊆ X → X ∈ AC _ A
22 simpr ⊢ X ∈ AC _ A ∧ x ∈ A ∧ B ⊆ X → B ⊆ X
23 21 22 ssexd ⊢ X ∈ AC _ A ∧ x ∈ A ∧ B ⊆ X → B ∈ V
24 7 fvmpt2 ⊢ x ∈ A ∧ B ∈ V → x ∈ A ⟼ B ⁡ x = B
25 20 23 24 syl2anc ⊢ X ∈ AC _ A ∧ x ∈ A ∧ B ⊆ X → x ∈ A ⟼ B ⁡ x = B
26 25 eleq2d ⊢ X ∈ AC _ A ∧ x ∈ A ∧ B ⊆ X → f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ↔ f ⁡ x ∈ B
27 26 ex ⊢ X ∈ AC _ A ∧ x ∈ A → B ⊆ X → f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ↔ f ⁡ x ∈ B
28 27 adantrd ⊢ X ∈ AC _ A ∧ x ∈ A → B ⊆ X ∧ B ≠ ∅ → f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ↔ f ⁡ x ∈ B
29 28 ralimdva ⊢ X ∈ AC _ A → ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ↔ f ⁡ x ∈ B
30 29 imp ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ↔ f ⁡ x ∈ B
31 ralbi ⊢ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ↔ f ⁡ x ∈ B → ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ↔ ∀ x ∈ A f ⁡ x ∈ B
32 30 31 syl ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ↔ ∀ x ∈ A f ⁡ x ∈ B
33 32 biimpa ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → ∀ x ∈ A f ⁡ x ∈ B
34 ssel ⊢ B ⊆ X → f ⁡ x ∈ B → f ⁡ x ∈ X
35 34 adantr ⊢ B ⊆ X ∧ B ≠ ∅ → f ⁡ x ∈ B → f ⁡ x ∈ X
36 35 ral2imi ⊢ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∀ x ∈ A f ⁡ x ∈ B → ∀ x ∈ A f ⁡ x ∈ X
37 19 33 36 sylc ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → ∀ x ∈ A f ⁡ x ∈ X
38 fveq2 ⊢ x = y → f ⁡ x = f ⁡ y
39 38 eleq1d ⊢ x = y → f ⁡ x ∈ X ↔ f ⁡ y ∈ X
40 39 rspccva ⊢ ∀ x ∈ A f ⁡ x ∈ X ∧ y ∈ A → f ⁡ y ∈ X
41 37 40 sylan ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x ∧ y ∈ A → f ⁡ y ∈ X
42 41 fmpttd ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → y ∈ A ⟼ f ⁡ y : A ⟶ X
43 simpll ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → X ∈ AC _ A
44 acnrcl ⊢ X ∈ AC _ A → A ∈ V
45 43 44 syl ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → A ∈ V
46 fex2 ⊢ y ∈ A ⟼ f ⁡ y : A ⟶ X ∧ A ∈ V ∧ X ∈ AC _ A → y ∈ A ⟼ f ⁡ y ∈ V
47 42 45 43 46 syl3anc ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → y ∈ A ⟼ f ⁡ y ∈ V
48 eqid ⊢ y ∈ A ⟼ f ⁡ y = y ∈ A ⟼ f ⁡ y
49 fvex ⊢ f ⁡ x ∈ V
50 15 48 49 fvmpt ⊢ x ∈ A → y ∈ A ⟼ f ⁡ y ⁡ x = f ⁡ x
51 50 eleq1d ⊢ x ∈ A → y ∈ A ⟼ f ⁡ y ⁡ x ∈ B ↔ f ⁡ x ∈ B
52 51 ralbiia ⊢ ∀ x ∈ A y ∈ A ⟼ f ⁡ y ⁡ x ∈ B ↔ ∀ x ∈ A f ⁡ x ∈ B
53 33 52 sylibr ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → ∀ x ∈ A y ∈ A ⟼ f ⁡ y ⁡ x ∈ B
54 42 53 jca ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → y ∈ A ⟼ f ⁡ y : A ⟶ X ∧ ∀ x ∈ A y ∈ A ⟼ f ⁡ y ⁡ x ∈ B
55 feq1 ⊢ g = y ∈ A ⟼ f ⁡ y → g : A ⟶ X ↔ y ∈ A ⟼ f ⁡ y : A ⟶ X
56 fveq1 ⊢ g = y ∈ A ⟼ f ⁡ y → g ⁡ x = y ∈ A ⟼ f ⁡ y ⁡ x
57 56 eleq1d ⊢ g = y ∈ A ⟼ f ⁡ y → g ⁡ x ∈ B ↔ y ∈ A ⟼ f ⁡ y ⁡ x ∈ B
58 57 ralbidv ⊢ g = y ∈ A ⟼ f ⁡ y → ∀ x ∈ A g ⁡ x ∈ B ↔ ∀ x ∈ A y ∈ A ⟼ f ⁡ y ⁡ x ∈ B
59 55 58 anbi12d ⊢ g = y ∈ A ⟼ f ⁡ y → g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ B ↔ y ∈ A ⟼ f ⁡ y : A ⟶ X ∧ ∀ x ∈ A y ∈ A ⟼ f ⁡ y ⁡ x ∈ B
60 47 54 59 spcedv ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ ∧ ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ B
61 60 ex ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∀ x ∈ A f ⁡ x ∈ x ∈ A ⟼ B ⁡ x → ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ B
62 18 61 syl5bi ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∀ y ∈ A f ⁡ y ∈ x ∈ A ⟼ B ⁡ y → ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ B
63 62 exlimdv ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∃ f ∀ y ∈ A f ⁡ y ∈ x ∈ A ⟼ B ⁡ y → ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ B
64 11 63 mpd ⊢ X ∈ AC _ A ∧ ∀ x ∈ A B ⊆ X ∧ B ≠ ∅ → ∃ g g : A ⟶ X ∧ ∀ x ∈ A g ⁡ x ∈ B