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

Step	Hyp	Ref	Expression
1		karden.1	. . . . . . . 8 |- A e. _V
2	1	enref 5654	. . . . . . 7 |- A ~~ A
3		breq1 3542	. . . . . . . 8 |- (w = A -> (w ~~ A <-> A ~~ A))
4	1, 3	cla4ev 2642	. . . . . . 7 |- (A ~~ A -> E.w w ~~ A)
5	2, 4	ax-mp 7	. . . . . 6 |- E.w w ~~ A
6		abn0 3131	. . . . . 6 |- ({w | w ~~ A} =/= (/) <-> E.w w ~~ A)
7	5, 6	mpbir 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)} = (/))
9	8	necon3bii 2326	. . . . 5 |- ({w | w ~~ A} =/= (/) <-> {z e. {w | w ~~ A} | A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)} =/= (/))
10	7, 9	mpbi 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))
12	10, 11	mpbi 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))
15	13, 14	elab 2675	. . . . . . 7 |- (z e. {w | w ~~ A} <-> z ~~ A)
16		breq1 3542	. . . . . . . 8 |- (w = y -> (w ~~ A <-> y ~~ A))
17	16	ralab 2688	. . . . . . 7 |- (A.y e. {w | w ~~ A} (rank` z) C_ (rank` y) <-> A.y(y ~~ A -> (rank` z) C_ (rank` y)))
18	15, 17	anbi12i 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)
20	19	a1i 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)))}
23	21, 22	eqeq12i 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)))))
25	23, 24	bitri 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))
28	27	sseq1d 2903	. . . . . . . . . . . . . . 15 |- (x = z -> ((rank` x) C_ (rank` y) <-> (rank` z) C_ (rank` y)))
29	28	imbi2d 380	. . . . . . . . . . . . . 14 |- (x = z -> ((y ~~ A -> (rank` x) C_ (rank` y)) <-> (y ~~ A -> (rank` z) C_ (rank` y))))
30	29	albidv 1954	. . . . . . . . . . . . 13 |- (x = z -> (A.y(y ~~ A -> (rank` x) C_ (rank` y)) <-> A.y(y ~~ A -> (rank` z) C_ (rank` y))))
31	26, 30	anbi12d 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))
33	28	imbi2d 380	. . . . . . . . . . . . . 14 |- (x = z -> ((y ~~ B -> (rank` x) C_ (rank` y)) <-> (y ~~ B -> (rank` z) C_ (rank` y))))
34	33	albidv 1954	. . . . . . . . . . . . 13 |- (x = z -> (A.y(y ~~ B -> (rank` x) C_ (rank` y)) <-> A.y(y ~~ B -> (rank` z) C_ (rank` y))))
35	32, 34	anbi12d 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)))))
36	31, 35	bibi12d 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))))))
37	36	a4v 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)))))
38	25, 37	sylbi 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)
40	38, 39	syl6bi 284	. . . . . . . 8 |- (C = D -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank` y))) -> z ~~ B))
41	20, 40	jcad 592	. . . . . . 7 |- (C = D -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank` y))) -> (z ~~ A /\ z ~~ B)))
42	1	ensym 5675	. . . . . . . 8 |- (z ~~ A -> A ~~ z)
43		entr 5677	. . . . . . . 8 |- ((A ~~ z /\ z ~~ B) -> A ~~ B)
44	42, 43	sylan 693	. . . . . . 7 |- ((z ~~ A /\ z ~~ B) -> A ~~ B)
45	41, 44	syl6 39	. . . . . 6 |- (C = D -> ((z ~~ A /\ A.y(y ~~ A -> (rank` z) C_ (rank` y))) -> A ~~ B))
46	18, 45	syl5bi 270	. . . . 5 |- (C = D -> ((z e. {w | w ~~ A} /\ A.y e. {w | w ~~ A} (rank` z) C_ (rank` y)) -> A ~~ B))
47	46	exp3a 496	. . . 4 |- (C = D -> (z e. {w | w ~~ A} -> (A.y e. {w | w ~~ A} (rank` z) C_ (rank` y) -> A ~~ B)))
48	47	r19.23adv 2493	. . 3 |- (C = D -> (E.z e. {w | w ~~ A}A.y e. {w | w ~~ A} (rank` z) C_ (rank` y) -> A ~~ B))
49	12, 48	mpi 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))
52	50, 51	mpan 773	. . . . 5 |- (A ~~ B -> (x ~~ A <-> x ~~ B))
53		enen2 5750	. . . . . . . 8 |- ((B e. _V /\ A ~~ B) -> (y ~~ A <-> y ~~ B))
54	50, 53	mpan 773	. . . . . . 7 |- (A ~~ B -> (y ~~ A <-> y ~~ B))
55	54	imbi1d 381	. . . . . 6 |- (A ~~ B -> ((y ~~ A -> (rank` x) C_ (rank` y)) <-> (y ~~ B -> (rank` x) C_ (rank` y))))
56	55	albidv 1954	. . . . 5 |- (A ~~ B -> (A.y(y ~~ A -> (rank` x) C_ (rank` y)) <-> A.y(y ~~ B -> (rank` x) C_ (rank` y))))
57	52, 56	anbi12d 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)))))
58	57	abbidv 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)))})
59	58, 21, 22	3eqtr4g 2230	. 2 |- (A ~~ B -> C = D)
60	49, 59	impbii 235	1 |- (C = D <-> A ~~ B)

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