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 eqtr4di 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 elrabi g y B | φ y B | φ g y B | φ B
46 45 ralimi x A g y B | φ y B | φ x A g y B | φ B
47 46 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
48 eqid x A g y B | φ = x A g y B | φ
49 48 fmpt x A g y B | φ B x A g y B | φ : A B
50 47 49 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
51 nfcv _ y B
52 51 elrabsf g y B | φ y B | φ g y B | φ B [˙ g y B | φ / y]˙ φ
53 52 simprbi g y B | φ y B | φ [˙ g y B | φ / y]˙ φ
54 53 ralimi x A g y B | φ y B | φ x A [˙ g y B | φ / y]˙ φ
55 54 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]˙ φ
56 50 55 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]˙ φ
57 feq1 f = x A g y B | φ f : A B x A g y B | φ : A B
58 nfmpt1 _ x x A g y B | φ
59 58 nfeq2 x f = x A g y B | φ
60 fvex f x V
61 60 1 sbcie [˙ f x / y]˙ φ ψ
62 fveq1 f = x A g y B | φ f x = x A g y B | φ x
63 fvex g y B | φ V
64 48 fvmpt2 x A g y B | φ V x A g y B | φ x = g y B | φ
65 63 64 mpan2 x A x A g y B | φ x = g y B | φ
66 62 65 sylan9eq f = x A g y B | φ x A f x = g y B | φ
67 66 sbceq1d f = x A g y B | φ x A [˙ f x / y]˙ φ [˙ g y B | φ / y]˙ φ
68 61 67 bitr3id f = x A g y B | φ x A ψ [˙ g y B | φ / y]˙ φ
69 59 68 ralbida f = x A g y B | φ x A ψ x A [˙ g y B | φ / y]˙ φ
70 57 69 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]˙ φ
71 44 56 70 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 ψ
72 71 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 ψ
73 42 72 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 ψ
74 73 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 ψ
75 32 74 mpd A V x A y B | φ dom card x A y B φ f f : A B x A ψ