Metamath Proof Explorer

Theorem infmap2

Description: An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of Jech p. 43. Although this version of infmap avoids the axiom of choice, it requires the powerset of an infinite set to be well-orderable and so is usually not applicable. (Contributed by NM, 1-Oct-2004) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion infmap2 
|- ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) -> ( A ^m B ) ~~ { x | ( x C_ A /\ x ~~ B ) } )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( B = (/) -> ( A ^m B ) = ( A ^m (/) ) )
2 breq2 
 |-  ( B = (/) -> ( x ~~ B <-> x ~~ (/) ) )
3 2 anbi2d 
 |-  ( B = (/) -> ( ( x C_ A /\ x ~~ B ) <-> ( x C_ A /\ x ~~ (/) ) ) )
4 3 abbidv 
 |-  ( B = (/) -> { x | ( x C_ A /\ x ~~ B ) } = { x | ( x C_ A /\ x ~~ (/) ) } )
5 1 4 breq12d 
 |-  ( B = (/) -> ( ( A ^m B ) ~~ { x | ( x C_ A /\ x ~~ B ) } <-> ( A ^m (/) ) ~~ { x | ( x C_ A /\ x ~~ (/) ) } ) )
6 simpl2 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> B ~<_ A )
7 reldom 
 |-  Rel ~<_
8 7 brrelex1i 
 |-  ( B ~<_ A -> B e. _V )
9 6 8 syl 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> B e. _V )
10 7 brrelex2i 
 |-  ( B ~<_ A -> A e. _V )
11 6 10 syl 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> A e. _V )
12 xpcomeng 
 |-  ( ( B e. _V /\ A e. _V ) -> ( B X. A ) ~~ ( A X. B ) )
13 9 11 12 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( B X. A ) ~~ ( A X. B ) )
14 simpl3 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( A ^m B ) e. dom card )
15 simpr 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> B =/= (/) )
16 mapdom3 
 |-  ( ( A e. _V /\ B e. _V /\ B =/= (/) ) -> A ~<_ ( A ^m B ) )
17 11 9 15 16 syl3anc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> A ~<_ ( A ^m B ) )
18 numdom 
 |-  ( ( ( A ^m B ) e. dom card /\ A ~<_ ( A ^m B ) ) -> A e. dom card )
19 14 17 18 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> A e. dom card )
20 simpl1 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> _om ~<_ A )
21 infxpabs 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A X. B ) ~~ A )
22 19 20 15 6 21 syl22anc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( A X. B ) ~~ A )
23 entr 
 |-  ( ( ( B X. A ) ~~ ( A X. B ) /\ ( A X. B ) ~~ A ) -> ( B X. A ) ~~ A )
24 13 22 23 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( B X. A ) ~~ A )
25 ssenen 
 |-  ( ( B X. A ) ~~ A -> { x | ( x C_ ( B X. A ) /\ x ~~ B ) } ~~ { x | ( x C_ A /\ x ~~ B ) } )
26 24 25 syl 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> { x | ( x C_ ( B X. A ) /\ x ~~ B ) } ~~ { x | ( x C_ A /\ x ~~ B ) } )
27 relen 
 |-  Rel ~~
28 27 brrelex1i 
 |-  ( { x | ( x C_ ( B X. A ) /\ x ~~ B ) } ~~ { x | ( x C_ A /\ x ~~ B ) } -> { x | ( x C_ ( B X. A ) /\ x ~~ B ) } e. _V )
29 26 28 syl 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> { x | ( x C_ ( B X. A ) /\ x ~~ B ) } e. _V )
30 abid2 
 |-  { x | x e. ( A ^m B ) } = ( A ^m B )
31 elmapi 
 |-  ( x e. ( A ^m B ) -> x : B --> A )
32 fssxp 
 |-  ( x : B --> A -> x C_ ( B X. A ) )
33 ffun 
 |-  ( x : B --> A -> Fun x )
34 vex 
 |-  x e. _V
35 34 fundmen 
 |-  ( Fun x -> dom x ~~ x )
36 ensym 
 |-  ( dom x ~~ x -> x ~~ dom x )
37 33 35 36 3syl 
 |-  ( x : B --> A -> x ~~ dom x )
38 fdm 
 |-  ( x : B --> A -> dom x = B )
39 37 38 breqtrd 
 |-  ( x : B --> A -> x ~~ B )
40 32 39 jca 
 |-  ( x : B --> A -> ( x C_ ( B X. A ) /\ x ~~ B ) )
41 31 40 syl 
 |-  ( x e. ( A ^m B ) -> ( x C_ ( B X. A ) /\ x ~~ B ) )
42 41 ss2abi 
 |-  { x | x e. ( A ^m B ) } C_ { x | ( x C_ ( B X. A ) /\ x ~~ B ) }
43 30 42 eqsstrri 
 |-  ( A ^m B ) C_ { x | ( x C_ ( B X. A ) /\ x ~~ B ) }
44 ssdomg 
 |-  ( { x | ( x C_ ( B X. A ) /\ x ~~ B ) } e. _V -> ( ( A ^m B ) C_ { x | ( x C_ ( B X. A ) /\ x ~~ B ) } -> ( A ^m B ) ~<_ { x | ( x C_ ( B X. A ) /\ x ~~ B ) } ) )
45 29 43 44 mpisyl 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( A ^m B ) ~<_ { x | ( x C_ ( B X. A ) /\ x ~~ B ) } )
46 domentr 
 |-  ( ( ( A ^m B ) ~<_ { x | ( x C_ ( B X. A ) /\ x ~~ B ) } /\ { x | ( x C_ ( B X. A ) /\ x ~~ B ) } ~~ { x | ( x C_ A /\ x ~~ B ) } ) -> ( A ^m B ) ~<_ { x | ( x C_ A /\ x ~~ B ) } )
47 45 26 46 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( A ^m B ) ~<_ { x | ( x C_ A /\ x ~~ B ) } )
48 ovex 
 |-  ( A ^m B ) e. _V
49 48 mptex 
 |-  ( f e. ( A ^m B ) |-> ran f ) e. _V
50 49 rnex 
 |-  ran ( f e. ( A ^m B ) |-> ran f ) e. _V
51 ensym 
 |-  ( x ~~ B -> B ~~ x )
52 51 ad2antll 
 |-  ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) -> B ~~ x )
53 bren 
 |-  ( B ~~ x <-> E. f f : B -1-1-onto-> x )
54 52 53 sylib 
 |-  ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) -> E. f f : B -1-1-onto-> x )
55 f1of 
 |-  ( f : B -1-1-onto-> x -> f : B --> x )
56 55 adantl 
 |-  ( ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) /\ f : B -1-1-onto-> x ) -> f : B --> x )
57 simplrl 
 |-  ( ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) /\ f : B -1-1-onto-> x ) -> x C_ A )
58 56 57 fssd 
 |-  ( ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) /\ f : B -1-1-onto-> x ) -> f : B --> A )
59 11 9 elmapd 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( f e. ( A ^m B ) <-> f : B --> A ) )
60 59 ad2antrr 
 |-  ( ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) /\ f : B -1-1-onto-> x ) -> ( f e. ( A ^m B ) <-> f : B --> A ) )
61 58 60 mpbird 
 |-  ( ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) /\ f : B -1-1-onto-> x ) -> f e. ( A ^m B ) )
62 f1ofo 
 |-  ( f : B -1-1-onto-> x -> f : B -onto-> x )
63 forn 
 |-  ( f : B -onto-> x -> ran f = x )
64 62 63 syl 
 |-  ( f : B -1-1-onto-> x -> ran f = x )
65 64 adantl 
 |-  ( ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) /\ f : B -1-1-onto-> x ) -> ran f = x )
66 65 eqcomd 
 |-  ( ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) /\ f : B -1-1-onto-> x ) -> x = ran f )
67 61 66 jca 
 |-  ( ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) /\ f : B -1-1-onto-> x ) -> ( f e. ( A ^m B ) /\ x = ran f ) )
68 67 ex 
 |-  ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) -> ( f : B -1-1-onto-> x -> ( f e. ( A ^m B ) /\ x = ran f ) ) )
69 68 eximdv 
 |-  ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) -> ( E. f f : B -1-1-onto-> x -> E. f ( f e. ( A ^m B ) /\ x = ran f ) ) )
70 54 69 mpd 
 |-  ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) -> E. f ( f e. ( A ^m B ) /\ x = ran f ) )
71 df-rex 
 |-  ( E. f e. ( A ^m B ) x = ran f <-> E. f ( f e. ( A ^m B ) /\ x = ran f ) )
72 70 71 sylibr 
 |-  ( ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) /\ ( x C_ A /\ x ~~ B ) ) -> E. f e. ( A ^m B ) x = ran f )
73 72 ex 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( ( x C_ A /\ x ~~ B ) -> E. f e. ( A ^m B ) x = ran f ) )
74 73 ss2abdv 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> { x | ( x C_ A /\ x ~~ B ) } C_ { x | E. f e. ( A ^m B ) x = ran f } )
75 eqid 
 |-  ( f e. ( A ^m B ) |-> ran f ) = ( f e. ( A ^m B ) |-> ran f )
76 75 rnmpt 
 |-  ran ( f e. ( A ^m B ) |-> ran f ) = { x | E. f e. ( A ^m B ) x = ran f }
77 74 76 sseqtrrdi 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> { x | ( x C_ A /\ x ~~ B ) } C_ ran ( f e. ( A ^m B ) |-> ran f ) )
78 ssdomg 
 |-  ( ran ( f e. ( A ^m B ) |-> ran f ) e. _V -> ( { x | ( x C_ A /\ x ~~ B ) } C_ ran ( f e. ( A ^m B ) |-> ran f ) -> { x | ( x C_ A /\ x ~~ B ) } ~<_ ran ( f e. ( A ^m B ) |-> ran f ) ) )
79 50 77 78 mpsyl 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> { x | ( x C_ A /\ x ~~ B ) } ~<_ ran ( f e. ( A ^m B ) |-> ran f ) )
80 vex 
 |-  f e. _V
81 80 rnex 
 |-  ran f e. _V
82 81 rgenw 
 |-  A. f e. ( A ^m B ) ran f e. _V
83 75 fnmpt 
 |-  ( A. f e. ( A ^m B ) ran f e. _V -> ( f e. ( A ^m B ) |-> ran f ) Fn ( A ^m B ) )
84 82 83 mp1i 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( f e. ( A ^m B ) |-> ran f ) Fn ( A ^m B ) )
85 dffn4 
 |-  ( ( f e. ( A ^m B ) |-> ran f ) Fn ( A ^m B ) <-> ( f e. ( A ^m B ) |-> ran f ) : ( A ^m B ) -onto-> ran ( f e. ( A ^m B ) |-> ran f ) )
86 84 85 sylib 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( f e. ( A ^m B ) |-> ran f ) : ( A ^m B ) -onto-> ran ( f e. ( A ^m B ) |-> ran f ) )
87 fodomnum 
 |-  ( ( A ^m B ) e. dom card -> ( ( f e. ( A ^m B ) |-> ran f ) : ( A ^m B ) -onto-> ran ( f e. ( A ^m B ) |-> ran f ) -> ran ( f e. ( A ^m B ) |-> ran f ) ~<_ ( A ^m B ) ) )
88 14 86 87 sylc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ran ( f e. ( A ^m B ) |-> ran f ) ~<_ ( A ^m B ) )
89 domtr 
 |-  ( ( { x | ( x C_ A /\ x ~~ B ) } ~<_ ran ( f e. ( A ^m B ) |-> ran f ) /\ ran ( f e. ( A ^m B ) |-> ran f ) ~<_ ( A ^m B ) ) -> { x | ( x C_ A /\ x ~~ B ) } ~<_ ( A ^m B ) )
90 79 88 89 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> { x | ( x C_ A /\ x ~~ B ) } ~<_ ( A ^m B ) )
91 sbth 
 |-  ( ( ( A ^m B ) ~<_ { x | ( x C_ A /\ x ~~ B ) } /\ { x | ( x C_ A /\ x ~~ B ) } ~<_ ( A ^m B ) ) -> ( A ^m B ) ~~ { x | ( x C_ A /\ x ~~ B ) } )
92 47 90 91 syl2anc 
 |-  ( ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) /\ B =/= (/) ) -> ( A ^m B ) ~~ { x | ( x C_ A /\ x ~~ B ) } )
93 7 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
94 93 3ad2ant1 
 |-  ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) -> A e. _V )
95 map0e 
 |-  ( A e. _V -> ( A ^m (/) ) = 1o )
96 94 95 syl 
 |-  ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) -> ( A ^m (/) ) = 1o )
97 1oex 
 |-  1o e. _V
98 97 enref 
 |-  1o ~~ 1o
99 df-sn 
 |-  { (/) } = { x | x = (/) }
100 df1o2 
 |-  1o = { (/) }
101 en0 
 |-  ( x ~~ (/) <-> x = (/) )
102 101 anbi2i 
 |-  ( ( x C_ A /\ x ~~ (/) ) <-> ( x C_ A /\ x = (/) ) )
103 0ss 
 |-  (/) C_ A
104 sseq1 
 |-  ( x = (/) -> ( x C_ A <-> (/) C_ A ) )
105 103 104 mpbiri 
 |-  ( x = (/) -> x C_ A )
106 105 pm4.71ri 
 |-  ( x = (/) <-> ( x C_ A /\ x = (/) ) )
107 102 106 bitr4i 
 |-  ( ( x C_ A /\ x ~~ (/) ) <-> x = (/) )
108 107 abbii 
 |-  { x | ( x C_ A /\ x ~~ (/) ) } = { x | x = (/) }
109 99 100 108 3eqtr4ri 
 |-  { x | ( x C_ A /\ x ~~ (/) ) } = 1o
110 98 109 breqtrri 
 |-  1o ~~ { x | ( x C_ A /\ x ~~ (/) ) }
111 96 110 eqbrtrdi 
 |-  ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) -> ( A ^m (/) ) ~~ { x | ( x C_ A /\ x ~~ (/) ) } )
112 5 92 111 pm2.61ne 
 |-  ( ( _om ~<_ A /\ B ~<_ A /\ ( A ^m B ) e. dom card ) -> ( A ^m B ) ~~ { x | ( x C_ A /\ x ~~ B ) } )