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 ψ