Metamath Proof Explorer

Theorem ac6sfi

Description: A version of ac6s for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009) (Proof shortened by Mario Carneiro, 29-Jan-2014)

Ref Expression
Hypothesis ac6sfi.1 ⊢ y = f ⁡ x → φ ↔ ψ
Assertion ac6sfi ⊢ A ∈ Fin ∧ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 ac6sfi.1 ⊢ y = f ⁡ x → φ ↔ ψ
2 raleq ⊢ u = ∅ → ∀ x ∈ u ∃ y ∈ B φ ↔ ∀ x ∈ ∅ ∃ y ∈ B φ
3 feq2 ⊢ u = ∅ → f : u ⟶ B ↔ f : ∅ ⟶ B
4 raleq ⊢ u = ∅ → ∀ x ∈ u ψ ↔ ∀ x ∈ ∅ ψ
5 3 4 anbi12d ⊢ u = ∅ → f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ f : ∅ ⟶ B ∧ ∀ x ∈ ∅ ψ
6 5 exbidv ⊢ u = ∅ → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∃ f f : ∅ ⟶ B ∧ ∀ x ∈ ∅ ψ
7 2 6 imbi12d ⊢ u = ∅ → ∀ x ∈ u ∃ y ∈ B φ → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∀ x ∈ ∅ ∃ y ∈ B φ → ∃ f f : ∅ ⟶ B ∧ ∀ x ∈ ∅ ψ
8 raleq ⊢ u = w → ∀ x ∈ u ∃ y ∈ B φ ↔ ∀ x ∈ w ∃ y ∈ B φ
9 feq2 ⊢ u = w → f : u ⟶ B ↔ f : w ⟶ B
10 raleq ⊢ u = w → ∀ x ∈ u ψ ↔ ∀ x ∈ w ψ
11 9 10 anbi12d ⊢ u = w → f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ f : w ⟶ B ∧ ∀ x ∈ w ψ
12 11 exbidv ⊢ u = w → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ
13 8 12 imbi12d ⊢ u = w → ∀ x ∈ u ∃ y ∈ B φ → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∀ x ∈ w ∃ y ∈ B φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ
14 raleq ⊢ u = w ∪ z → ∀ x ∈ u ∃ y ∈ B φ ↔ ∀ x ∈ w ∪ z ∃ y ∈ B φ
15 feq2 ⊢ u = w ∪ z → f : u ⟶ B ↔ f : w ∪ z ⟶ B
16 raleq ⊢ u = w ∪ z → ∀ x ∈ u ψ ↔ ∀ x ∈ w ∪ z ψ
17 15 16 anbi12d ⊢ u = w ∪ z → f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ f : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z ψ
18 17 exbidv ⊢ u = w ∪ z → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∃ f f : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z ψ
19 feq1 ⊢ f = g → f : w ∪ z ⟶ B ↔ g : w ∪ z ⟶ B
20 fvex ⊢ f ⁡ x ∈ V
21 20 1 sbcie ⊢ [˙ f ⁡ x / y]˙ φ ↔ ψ
22 fveq1 ⊢ f = g → f ⁡ x = g ⁡ x
23 22 sbceq1d ⊢ f = g → [˙ f ⁡ x / y]˙ φ ↔ [˙ g ⁡ x / y]˙ φ
24 21 23 bitr3id ⊢ f = g → ψ ↔ [˙ g ⁡ x / y]˙ φ
25 24 ralbidv ⊢ f = g → ∀ x ∈ w ∪ z ψ ↔ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
26 19 25 anbi12d ⊢ f = g → f : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z ψ ↔ g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
27 26 cbvexvw ⊢ ∃ f f : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z ψ ↔ ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
28 18 27 bitrdi ⊢ u = w ∪ z → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
29 14 28 imbi12d ⊢ u = w ∪ z → ∀ x ∈ u ∃ y ∈ B φ → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
30 raleq ⊢ u = A → ∀ x ∈ u ∃ y ∈ B φ ↔ ∀ x ∈ A ∃ y ∈ B φ
31 feq2 ⊢ u = A → f : u ⟶ B ↔ f : A ⟶ B
32 raleq ⊢ u = A → ∀ x ∈ u ψ ↔ ∀ x ∈ A ψ
33 31 32 anbi12d ⊢ u = A → f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ f : A ⟶ B ∧ ∀ x ∈ A ψ
34 33 exbidv ⊢ u = A → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
35 30 34 imbi12d ⊢ u = A → ∀ x ∈ u ∃ y ∈ B φ → ∃ f f : u ⟶ B ∧ ∀ x ∈ u ψ ↔ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
36 f0 ⊢ ∅ : ∅ ⟶ B
37 0ex ⊢ ∅ ∈ V
38 ral0 ⊢ ∀ x ∈ ∅ ψ
39 38 biantru ⊢ f : ∅ ⟶ B ↔ f : ∅ ⟶ B ∧ ∀ x ∈ ∅ ψ
40 feq1 ⊢ f = ∅ → f : ∅ ⟶ B ↔ ∅ : ∅ ⟶ B
41 39 40 bitr3id ⊢ f = ∅ → f : ∅ ⟶ B ∧ ∀ x ∈ ∅ ψ ↔ ∅ : ∅ ⟶ B
42 37 41 spcev ⊢ ∅ : ∅ ⟶ B → ∃ f f : ∅ ⟶ B ∧ ∀ x ∈ ∅ ψ
43 36 42 mp1i ⊢ ∀ x ∈ ∅ ∃ y ∈ B φ → ∃ f f : ∅ ⟶ B ∧ ∀ x ∈ ∅ ψ
44 ssun1 ⊢ w ⊆ w ∪ z
45 ssralv ⊢ w ⊆ w ∪ z → ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∀ x ∈ w ∃ y ∈ B φ
46 44 45 ax-mp ⊢ ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∀ x ∈ w ∃ y ∈ B φ
47 46 imim1i ⊢ ∀ x ∈ w ∃ y ∈ B φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ
48 ssun2 ⊢ z ⊆ w ∪ z
49 ssralv ⊢ z ⊆ w ∪ z → ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∀ x ∈ z ∃ y ∈ B φ
50 48 49 ax-mp ⊢ ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∀ x ∈ z ∃ y ∈ B φ
51 ralsnsg ⊢ z ∈ V → ∀ x ∈ z ∃ y ∈ B φ ↔ [˙z / x]˙ ∃ y ∈ B φ
52 51 elv ⊢ ∀ x ∈ z ∃ y ∈ B φ ↔ [˙z / x]˙ ∃ y ∈ B φ
53 sbcrex ⊢ [˙z / x]˙ ∃ y ∈ B φ ↔ ∃ y ∈ B [˙z / x]˙ φ
54 52 53 bitri ⊢ ∀ x ∈ z ∃ y ∈ B φ ↔ ∃ y ∈ B [˙z / x]˙ φ
55 50 54 sylib ⊢ ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∃ y ∈ B [˙z / x]˙ φ
56 nfv ⊢ Ⅎ y ¬ z ∈ w
57 nfv ⊢ Ⅎ y ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ
58 nfv ⊢ Ⅎ y g : w ∪ z ⟶ B
59 nfcv ⊢ Ⅎ _ y w ∪ z
60 nfsbc1v ⊢ Ⅎ y [˙ g ⁡ x / y]˙ φ
61 59 60 nfralw ⊢ Ⅎ y ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
62 58 61 nfan ⊢ Ⅎ y g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
63 62 nfex ⊢ Ⅎ y ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
64 57 63 nfim ⊢ Ⅎ y ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
65 simprl ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → f : w ⟶ B
66 vex ⊢ z ∈ V
67 vex ⊢ y ∈ V
68 66 67 f1osn ⊢ z y : z ⟶ 1-1 onto y
69 f1of ⊢ z y : z ⟶ 1-1 onto y → z y : z ⟶ y
70 68 69 mp1i ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → z y : z ⟶ y
71 simpl2 ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → y ∈ B
72 71 snssd ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → y ⊆ B
73 70 72 fssd ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → z y : z ⟶ B
74 simpl1 ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → ¬ z ∈ w
75 disjsn ⊢ w ∩ z = ∅ ↔ ¬ z ∈ w
76 74 75 sylibr ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → w ∩ z = ∅
77 65 73 76 fun2d ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → f ∪ z y : w ∪ z ⟶ B
78 simprr ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ w ψ
79 eleq1a ⊢ x ∈ w → z = x → z ∈ w
80 79 necon3bd ⊢ x ∈ w → ¬ z ∈ w → z ≠ x
81 80 impcom ⊢ ¬ z ∈ w ∧ x ∈ w → z ≠ x
82 fvunsn ⊢ z ≠ x → f ∪ z y ⁡ x = f ⁡ x
83 dfsbcq ⊢ f ∪ z y ⁡ x = f ⁡ x → [˙ f ∪ z y ⁡ x / y]˙ φ ↔ [˙ f ⁡ x / y]˙ φ
84 83 21 bitr2di ⊢ f ∪ z y ⁡ x = f ⁡ x → ψ ↔ [˙ f ∪ z y ⁡ x / y]˙ φ
85 81 82 84 3syl ⊢ ¬ z ∈ w ∧ x ∈ w → ψ ↔ [˙ f ∪ z y ⁡ x / y]˙ φ
86 85 ralbidva ⊢ ¬ z ∈ w → ∀ x ∈ w ψ ↔ ∀ x ∈ w [˙ f ∪ z y ⁡ x / y]˙ φ
87 74 86 syl ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ w ψ ↔ ∀ x ∈ w [˙ f ∪ z y ⁡ x / y]˙ φ
88 78 87 mpbid ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ w [˙ f ∪ z y ⁡ x / y]˙ φ
89 simpl3 ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → [˙z / x]˙ φ
90 ffun ⊢ f ∪ z y : w ∪ z ⟶ B → Fun ⁡ f ∪ z y
91 ssun2 ⊢ z y ⊆ f ∪ z y
92 vsnid ⊢ z ∈ z
93 67 dmsnop ⊢ dom ⁡ z y = z
94 92 93 eleqtrri ⊢ z ∈ dom ⁡ z y
95 funssfv ⊢ Fun ⁡ f ∪ z y ∧ z y ⊆ f ∪ z y ∧ z ∈ dom ⁡ z y → f ∪ z y ⁡ z = z y ⁡ z
96 91 94 95 mp3an23 ⊢ Fun ⁡ f ∪ z y → f ∪ z y ⁡ z = z y ⁡ z
97 77 90 96 3syl ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → f ∪ z y ⁡ z = z y ⁡ z
98 66 67 fvsn ⊢ z y ⁡ z = y
99 97 98 eqtr2di ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → y = f ∪ z y ⁡ z
100 ralsnsg ⊢ z ∈ V → ∀ x ∈ z φ ↔ [˙z / x]˙ φ
101 100 elv ⊢ ∀ x ∈ z φ ↔ [˙z / x]˙ φ
102 elsni ⊢ x ∈ z → x = z
103 102 fveq2d ⊢ x ∈ z → f ∪ z y ⁡ x = f ∪ z y ⁡ z
104 103 eqeq2d ⊢ x ∈ z → y = f ∪ z y ⁡ x ↔ y = f ∪ z y ⁡ z
105 104 biimparc ⊢ y = f ∪ z y ⁡ z ∧ x ∈ z → y = f ∪ z y ⁡ x
106 sbceq1a ⊢ y = f ∪ z y ⁡ x → φ ↔ [˙ f ∪ z y ⁡ x / y]˙ φ
107 105 106 syl ⊢ y = f ∪ z y ⁡ z ∧ x ∈ z → φ ↔ [˙ f ∪ z y ⁡ x / y]˙ φ
108 107 ralbidva ⊢ y = f ∪ z y ⁡ z → ∀ x ∈ z φ ↔ ∀ x ∈ z [˙ f ∪ z y ⁡ x / y]˙ φ
109 101 108 bitr3id ⊢ y = f ∪ z y ⁡ z → [˙z / x]˙ φ ↔ ∀ x ∈ z [˙ f ∪ z y ⁡ x / y]˙ φ
110 99 109 syl ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → [˙z / x]˙ φ ↔ ∀ x ∈ z [˙ f ∪ z y ⁡ x / y]˙ φ
111 89 110 mpbid ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ z [˙ f ∪ z y ⁡ x / y]˙ φ
112 ralun ⊢ ∀ x ∈ w [˙ f ∪ z y ⁡ x / y]˙ φ ∧ ∀ x ∈ z [˙ f ∪ z y ⁡ x / y]˙ φ → ∀ x ∈ w ∪ z [˙ f ∪ z y ⁡ x / y]˙ φ
113 88 111 112 syl2anc ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ w ∪ z [˙ f ∪ z y ⁡ x / y]˙ φ
114 vex ⊢ f ∈ V
115 snex ⊢ z y ∈ V
116 114 115 unex ⊢ f ∪ z y ∈ V
117 feq1 ⊢ g = f ∪ z y → g : w ∪ z ⟶ B ↔ f ∪ z y : w ∪ z ⟶ B
118 fveq1 ⊢ g = f ∪ z y → g ⁡ x = f ∪ z y ⁡ x
119 118 sbceq1d ⊢ g = f ∪ z y → [˙ g ⁡ x / y]˙ φ ↔ [˙ f ∪ z y ⁡ x / y]˙ φ
120 119 ralbidv ⊢ g = f ∪ z y → ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ ↔ ∀ x ∈ w ∪ z [˙ f ∪ z y ⁡ x / y]˙ φ
121 117 120 anbi12d ⊢ g = f ∪ z y → g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ ↔ f ∪ z y : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ f ∪ z y ⁡ x / y]˙ φ
122 116 121 spcev ⊢ f ∪ z y : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ f ∪ z y ⁡ x / y]˙ φ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
123 77 113 122 syl2anc ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ ∧ f : w ⟶ B ∧ ∀ x ∈ w ψ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
124 123 ex ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ → f : w ⟶ B ∧ ∀ x ∈ w ψ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
125 124 exlimdv ⊢ ¬ z ∈ w ∧ y ∈ B ∧ [˙z / x]˙ φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
126 125 3exp ⊢ ¬ z ∈ w → y ∈ B → [˙z / x]˙ φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
127 56 64 126 rexlimd ⊢ ¬ z ∈ w → ∃ y ∈ B [˙z / x]˙ φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
128 55 127 syl5 ⊢ ¬ z ∈ w → ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
129 128 a2d ⊢ ¬ z ∈ w → ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
130 47 129 syl5 ⊢ ¬ z ∈ w → ∀ x ∈ w ∃ y ∈ B φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
131 130 adantl ⊢ w ∈ Fin ∧ ¬ z ∈ w → ∀ x ∈ w ∃ y ∈ B φ → ∃ f f : w ⟶ B ∧ ∀ x ∈ w ψ → ∀ x ∈ w ∪ z ∃ y ∈ B φ → ∃ g g : w ∪ z ⟶ B ∧ ∀ x ∈ w ∪ z [˙ g ⁡ x / y]˙ φ
132 7 13 29 35 43 131 findcard2s ⊢ A ∈ Fin → ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ
133 132 imp ⊢ A ∈ Fin ∧ ∀ x ∈ A ∃ y ∈ B φ → ∃ f f : A ⟶ B ∧ ∀ x ∈ A ψ