Metamath Proof Explorer


Theorem ac6num

Description: A version of ac6 which takes the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis ac6num.1 y = f x φ ψ
Assertion ac6num A V x A y B | φ dom card x A y B φ f f : A B x A ψ

Proof

Step Hyp Ref Expression
1 ac6num.1 y = f x φ ψ
2 nfiu1 _ x x A y B | φ
3 2 nfel1 x x A y B | φ dom card
4 ssiun2 x A y B | φ x A y B | φ
5 ssexg y B | φ x A y B | φ x A y B | φ dom card y B | φ V
6 5 expcom x A y B | φ dom card y B | φ x A y B | φ y B | φ V
7 4 6 syl5 x A y B | φ dom card x A y B | φ V
8 3 7 ralrimi x A y B | φ dom card x A y B | φ V
9 dfiun2g x A y B | φ V x A y B | φ = z | x A z = y B | φ
10 8 9 syl x A y B | φ dom card x A y B | φ = z | x A z = y B | φ
11 eqid x A y B | φ = x A y B | φ
12 11 rnmpt ran x A y B | φ = z | x A z = y B | φ
13 12 unieqi ran x A y B | φ = z | x A z = y B | φ
14 10 13 syl6eqr x A y B | φ dom card x A y B | φ = ran x A y B | φ
15 id x A y B | φ dom card x A y B | φ dom card
16 14 15 eqeltrrd x A y B | φ dom card ran x A y B | φ dom card
17 16 3ad2ant2 A V x A y B | φ dom card x A y B φ ran x A y B | φ dom card
18 simp3 A V x A y B | φ dom card x A y B φ x A y B φ
19 necom y B | φ y B | φ
20 rabn0 y B | φ y B φ
21 df-ne y B | φ ¬ = y B | φ
22 19 20 21 3bitr3i y B φ ¬ = y B | φ
23 22 ralbii x A y B φ x A ¬ = y B | φ
24 ralnex x A ¬ = y B | φ ¬ x A = y B | φ
25 23 24 bitri x A y B φ ¬ x A = y B | φ
26 18 25 sylib A V x A y B | φ dom card x A y B φ ¬ x A = y B | φ
27 0ex V
28 11 elrnmpt V ran x A y B | φ x A = y B | φ
29 27 28 ax-mp ran x A y B | φ x A = y B | φ
30 26 29 sylnibr A V x A y B | φ dom card x A y B φ ¬ ran x A y B | φ
31 ac5num ran x A y B | φ dom card ¬ ran x A y B | φ g g : ran x A y B | φ ran x A y B | φ z ran x A y B | φ g z z
32 17 30 31 syl2anc A V x A y B | φ dom card x A y B φ g g : ran x A y B | φ ran x A y B | φ z ran x A y B | φ g z z
33 ffn g : ran x A y B | φ ran x A y B | φ g Fn ran x A y B | φ
34 33 anim1i g : ran x A y B | φ ran x A y B | φ z ran x A y B | φ g z z g Fn ran x A y B | φ z ran x A y B | φ g z z
35 8 3ad2ant2 A V x A y B | φ dom card x A y B φ x A y B | φ V
36 fveq2 z = y B | φ g z = g y B | φ
37 id z = y B | φ z = y B | φ
38 36 37 eleq12d z = y B | φ g z z g y B | φ y B | φ
39 11 38 ralrnmptw x A y B | φ V z ran x A y B | φ g z z x A g y B | φ y B | φ
40 35 39 syl A V x A y B | φ dom card x A y B φ z ran x A y B | φ g z z x A g y B | φ y B | φ
41 40 anbi2d A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ z ran x A y B | φ g z z g Fn ran x A y B | φ x A g y B | φ y B | φ
42 34 41 syl5ib A V x A y B | φ dom card x A y B φ g : ran x A y B | φ ran x A y B | φ z ran x A y B | φ g z z g Fn ran x A y B | φ x A g y B | φ y B | φ
43 simpl1 A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ x A g y B | φ y B | φ A V
44 43 mptexd A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ x A g y B | φ y B | φ x A g y B | φ V
45 ssrab2 y B | φ B
46 45 sseli g y B | φ y B | φ g y B | φ B
47 46 ralimi x A g y B | φ y B | φ x A g y B | φ B
48 47 ad2antll A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ x A g y B | φ y B | φ x A g y B | φ B
49 eqid x A g y B | φ = x A g y B | φ
50 49 fmpt x A g y B | φ B x A g y B | φ : A B
51 48 50 sylib A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ x A g y B | φ y B | φ x A g y B | φ : A B
52 nfcv _ y B
53 52 elrabsf g y B | φ y B | φ g y B | φ B [˙ g y B | φ / y]˙ φ
54 53 simprbi g y B | φ y B | φ [˙ g y B | φ / y]˙ φ
55 54 ralimi x A g y B | φ y B | φ x A [˙ g y B | φ / y]˙ φ
56 55 ad2antll A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ x A g y B | φ y B | φ x A [˙ g y B | φ / y]˙ φ
57 51 56 jca A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ x A g y B | φ y B | φ x A g y B | φ : A B x A [˙ g y B | φ / y]˙ φ
58 feq1 f = x A g y B | φ f : A B x A g y B | φ : A B
59 nfmpt1 _ x x A g y B | φ
60 59 nfeq2 x f = x A g y B | φ
61 fvex f x V
62 61 1 sbcie [˙ f x / y]˙ φ ψ
63 fveq1 f = x A g y B | φ f x = x A g y B | φ x
64 fvex g y B | φ V
65 49 fvmpt2 x A g y B | φ V x A g y B | φ x = g y B | φ
66 64 65 mpan2 x A x A g y B | φ x = g y B | φ
67 63 66 sylan9eq f = x A g y B | φ x A f x = g y B | φ
68 67 sbceq1d f = x A g y B | φ x A [˙ f x / y]˙ φ [˙ g y B | φ / y]˙ φ
69 62 68 syl5bbr f = x A g y B | φ x A ψ [˙ g y B | φ / y]˙ φ
70 60 69 ralbida f = x A g y B | φ x A ψ x A [˙ g y B | φ / y]˙ φ
71 58 70 anbi12d f = x A g y B | φ f : A B x A ψ x A g y B | φ : A B x A [˙ g y B | φ / y]˙ φ
72 44 57 71 spcedv A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ x A g y B | φ y B | φ f f : A B x A ψ
73 72 ex A V x A y B | φ dom card x A y B φ g Fn ran x A y B | φ x A g y B | φ y B | φ f f : A B x A ψ
74 42 73 syld A V x A y B | φ dom card x A y B φ g : ran x A y B | φ ran x A y B | φ z ran x A y B | φ g z z f f : A B x A ψ
75 74 exlimdv A V x A y B | φ dom card x A y B φ g g : ran x A y B | φ ran x A y B | φ z ran x A y B | φ g z z f f : A B x A ψ
76 32 75 mpd A V x A y B | φ dom card x A y B φ f f : A B x A ψ