HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem karden 6160
Description: If we allow the Axiom of Regularity, we can avoid the Axiom of Choice by defining the cardinal number of a set as the set of all sets equinumerous to it and having least possible rank. This theorem proves the equinumerosity relationship for this definition (compare carden 6470). The hypotheses correspond to the definition of kard of [Enderton] p. 222 (which we don't define separately since currently we do not use it elsewhere). This theorem along with kardex 6159 justify the definition of kard. The restriction to least rank prevents the proper class that would result from {x | x ~~ A}.
Hypotheses
Ref Expression
karden.1 |- A e. _V
karden.2 |- B e. _V
karden.3 |- C = {x | (x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y)))}
karden.4 |- D = {x | (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))}
Assertion
Ref Expression
karden |- (C = D <-> A ~~ B)
Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem karden
StepHypRef Expression
1 karden.1 . . . . . . . 8 |- A e. _V
21enref 5654 . . . . . . 7 |- A ~~ A
3 breq1 3542 . . . . . . . 8 |- (w = A -> (w ~~ A <-> A ~~ A))
41, 3cla4ev 2642 . . . . . . 7 |- (A ~~ A -> E.w w ~~ A)
52, 4ax-mp 7 . . . . . 6 |- E.w w ~~ A
6 abn0 3131 . . . . . 6 |- ({w | w ~~ A} =/= (/) <-> E.w w ~~ A)
75, 6mpbir 255 . . . . 5 |- {w | w ~~ A} =/= (/)
8 scott0 6151 . . . . . 6 |- ({w | w ~~ A} = (/) <-> {z e. {w | w ~~ A} | A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)} = (/))
98necon3bii 2326 . . . . 5 |- ({w | w ~~ A} =/= (/) <-> {z e. {w | w ~~ A} | A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)} =/= (/))
107, 9mpbi 254 . . . 4 |- {z e. {w | w ~~ A} | A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)} =/= (/)
11 rabn0 3132 . . . 4 |- ({z e. {w | w ~~ A} | A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)} =/= (/) <-> E.z e. {w | w ~~ A}A.y e. {w | w ~~ A} (rank` z) C_ (rank` y))
1210, 11mpbi 254 . . 3 |- E.z e. {w | w ~~ A}A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)
13 visset 2572 . . . . . . . 8 |- z e. _V
14 breq1 3542 . . . . . . . 8 |- (w = z -> (w ~~ A <-> z ~~ A))
1513, 14elab 2675 . . . . . . 7 |- (z e. {w | w ~~ A} <-> z ~~ A)
16 breq1 3542 . . . . . . . 8 |- (w = y -> (w ~~ A <-> y ~~ A))
1716ralab 2688 . . . . . . 7 |- (A.y e. {w | w ~~ A} (rank` z) C_ (rank` y) <-> A.y(y ~~ A -> (rank` z) C_ (rank` y)))
1815, 17anbi12i 806 . . . . . 6 |- ((z e. {w | w ~~ A} /\ A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)) <-> (z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank` y))))
19 simpl 533 . . . . . . . . 9 |- ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank` y))) -> z ~~ A)
2019a1i 8 . . . . . . . 8 |- (C = D -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank`
y))) -> z ~~ A))
21 karden.3 . . . . . . . . . . . 12 |- C = {x | (x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y)))}
22 karden.4 . . . . . . . . . . . 12 |- D = {x | (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))}
2321, 22eqeq12i 2183 . . . . . . . . . . 11 |- (C = D <-> {x | (x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y)))} = {x | (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))})
24 eq2ab 2282 . . . . . . . . . . 11 |- ({x | (x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y)))} = {x | (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))} <-> A.x((x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y))) <-> (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))))
2523, 24bitri 306 . . . . . . . . . 10 |- (C = D <-> A.x((x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y))) <-> (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))))
26 breq1 3542 . . . . . . . . . . . . 13 |- (x = z -> (x ~~ A <-> z ~~ A))
27 fveq2 4804 . . . . . . . . . . . . . . . 16 |- (x = z -> (rank` x) = (rank`
z))
2827sseq1d 2903 . . . . . . . . . . . . . . 15 |- (x = z -> ((rank` x) C_ (rank` y) <-> (rank` z) C_ (rank` y)))
2928imbi2d 380 . . . . . . . . . . . . . 14 |- (x = z -> ((y ~~ A -> (rank` x) C_ (rank` y)) <-> (y ~~ A -> (rank` z) C_ (rank`
y))))
3029albidv 1954 . . . . . . . . . . . . 13 |- (x = z -> (A.y(y ~~ A -> (rank` x) C_ (rank` y)) <-> A.y(y ~~ A -> (rank` z) C_ (rank` y))))
3126, 30anbi12d 821 . . . . . . . . . . . 12 |- (x = z -> ((x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y))) <-> (z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank` y)))))
32 breq1 3542 . . . . . . . . . . . . 13 |- (x = z -> (x ~~ B <-> z ~~ B))
3328imbi2d 380 . . . . . . . . . . . . . 14 |- (x = z -> ((y ~~ B -> (rank` x) C_ (rank` y)) <-> (y ~~ B -> (rank` z) C_ (rank`
y))))
3433albidv 1954 . . . . . . . . . . . . 13 |- (x = z -> (A.y(y ~~ B -> (rank` x) C_ (rank` y)) <-> A.y(y ~~ B -> (rank` z) C_ (rank` y))))
3532, 34anbi12d 821 . . . . . . . . . . . 12 |- (x = z -> ((x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y))) <-> (z ~~ B /\ A.y(y ~~ B -> (rank` z) C_ (rank` y)))))
3631, 35bibi12d 385 . . . . . . . . . . 11 |- (x = z -> (((x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y))) <-> (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))) <-> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank` y))) <-> (z ~~ B /\ A.y(y ~~ B -> (rank` z) C_ (rank`
y))))))
3736a4v 1948 . . . . . . . . . 10 |- (A.x((x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y))) <-> (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))) -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank` y))) <-> (z ~~ B /\ A.y(y ~~ B -> (rank` z) C_ (rank` y)))))
3825, 37sylbi 237 . . . . . . . . 9 |- (C = D -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank`
y))) <-> (z ~~ B /\ A.y(y ~~ B -> (rank` z) C_ (rank`
y)))))
39 simpl 533 . . . . . . . . 9 |- ((z ~~ B /\ A.y(y ~~ B -> (rank` z) C_ (rank` y))) -> z ~~ B)
4038, 39syl6bi 284 . . . . . . . 8 |- (C = D -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank`
y))) -> z ~~ B))
4120, 40jcad 592 . . . . . . 7 |- (C = D -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank`
y))) -> (z ~~ A /\ z ~~ B)))
421ensym 5675 . . . . . . . 8 |- (z ~~ A -> A ~~ z)
43 entr 5677 . . . . . . . 8 |- ((A ~~ z /\ z ~~ B) -> A ~~ B)
4442, 43sylan 693 . . . . . . 7 |- ((z ~~ A /\ z ~~ B) -> A ~~ B)
4541, 44syl6 39 . . . . . 6 |- (C = D -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank`
y))) -> A ~~ B))
4618, 45syl5bi 270 . . . . 5 |- (C = D -> ((z e. {w | w ~~ A} /\ A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)) -> A ~~ B))
4746exp3a 496 . . . 4 |- (C = D -> (z e. {w | w ~~ A} -> (A.y e. {w | w ~~ A} (rank` z) C_ (rank` y) -> A ~~ B)))
4847r19.23adv 2493 . . 3 |- (C = D -> (E.z e. {w | w ~~ A}A.y e. {w | w ~~ A} (rank` z) C_ (rank` y) -> A ~~ B))
4912, 48mpi 101 . 2 |- (C = D -> A ~~ B)
50 karden.2 . . . . . 6 |- B e. _V
51 enen2 5750 . . . . . 6 |- ((B e. _V /\ A ~~ B) -> (x ~~ A <-> x ~~ B))
5250, 51mpan 773 . . . . 5 |- (A ~~ B -> (x ~~ A <-> x ~~ B))
53 enen2 5750 . . . . . . . 8 |- ((B e. _V /\ A ~~ B) -> (y ~~ A <-> y ~~ B))
5450, 53mpan 773 . . . . . . 7 |- (A ~~ B -> (y ~~ A <-> y ~~ B))
5554imbi1d 381 . . . . . 6 |- (A ~~ B -> ((y ~~ A -> (rank` x) C_ (rank` y)) <-> (y ~~ B -> (rank` x) C_ (rank` y))))
5655albidv 1954 . . . . 5 |- (A ~~ B -> (A.y(y ~~ A -> (rank` x) C_ (rank` y)) <-> A.y(y ~~ B -> (rank` x) C_ (rank` y))))
5752, 56anbi12d 821 . . . 4 |- (A ~~ B -> ((x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y))) <-> (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))))
5857abbidv 2286 . . 3 |- (A ~~ B -> {x | (x ~~ A /\ A.y(y ~~ A -> (rank` x) C_ (rank` y)))} = {x | (x ~~ B /\ A.y(y ~~ B -> (rank` x) C_ (rank` y)))})
5958, 21, 223eqtr4g 2230 . 2 |- (A ~~ B -> C = D)
6049, 59impbii 235 1 |- (C = D <-> A ~~ B)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433  A.wal 1613   = wceq 1615   e. wcel 1617  E.wex 1644  {cab 2157   =/= wne 2295  A.wral 2385  E.wrex 2386  {crab 2388  _Vcvv 2569   C_ wss 2859  (/)c0 3114   class class class wbr 3539  ` cfv 4163   ~~ cen 5627  rankcrnk 6030
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961
This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iin 3471  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-er 5519  df-en 5631  df-rank 6032
Copyright terms: Public domain