Theorem karden

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 the least possible rank. This theorem proves the equinumerosity relationship for this definition (compare carden ). 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 justify the definition of kard. The restriction to the least rank prevents the proper class that would result from { x | x ~A } . (Contributed by NM, 18-Dec-2003) (Revised by AV, 12-Jul-2022)

	Ref	Expression
Hypotheses	karden.a	⊢ 𝐴 ∈ V
	karden.c	⊢ 𝐶 = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
	karden.d	⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
Assertion	karden	⊢ ( 𝐶 = 𝐷 ↔ 𝐴 ≈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		karden.a	⊢ 𝐴 ∈ V
2		karden.c	⊢ 𝐶 = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
3		karden.d	⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
4		breq1	⊢ ( 𝑤 = 𝐴 → ( 𝑤 ≈ 𝐴 ↔ 𝐴 ≈ 𝐴 ) )
5	1	enref	⊢ 𝐴 ≈ 𝐴
6	1 4 5	ceqsexv2d	⊢ ∃ 𝑤 𝑤 ≈ 𝐴
7		abn0	⊢ ( { 𝑤 ∣ 𝑤 ≈ 𝐴 } ≠ ∅ ↔ ∃ 𝑤 𝑤 ≈ 𝐴 )
8	6 7	mpbir	⊢ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ≠ ∅
9		scott0	⊢ ( { 𝑤 ∣ 𝑤 ≈ 𝐴 } = ∅ ↔ { 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )
10	9	necon3bii	⊢ ( { 𝑤 ∣ 𝑤 ≈ 𝐴 } ≠ ∅ ↔ { 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ )
11	8 10	mpbi	⊢ { 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅
12		rabn0	⊢ ( { 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ ↔ ∃ 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) )
13	11 12	mpbi	⊢ ∃ 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 )
14		vex	⊢ 𝑧 ∈ V
15		breq1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ≈ 𝐴 ↔ 𝑧 ≈ 𝐴 ) )
16	14 15	elab	⊢ ( 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ↔ 𝑧 ≈ 𝐴 )
17		breq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ≈ 𝐴 ↔ 𝑦 ≈ 𝐴 ) )
18	17	ralab	⊢ ( ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) )
19	16 18	anbi12i	⊢ ( ( 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
20		simpl	⊢ ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝑧 ≈ 𝐴 )
21	20	a1i	⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝑧 ≈ 𝐴 ) )
22	2 3	eqeq12i	⊢ ( 𝐶 = 𝐷 ↔ { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } )
23		abbi	⊢ ( ∀ 𝑥 ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) ↔ { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } )
24	22 23	bitr4i	⊢ ( 𝐶 = 𝐷 ↔ ∀ 𝑥 ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
25		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≈ 𝐴 ↔ 𝑧 ≈ 𝐴 ) )
26		fveq2	⊢ ( 𝑥 = 𝑧 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑧 ) )
27	26	sseq1d	⊢ ( 𝑥 = 𝑧 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) )
28	27	imbi2d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
29	28	albidv	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
30	25 29	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
31		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≈ 𝐵 ↔ 𝑧 ≈ 𝐵 ) )
32	27	imbi2d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
33	32	albidv	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
34	31 33	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
35	30 34	bibi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) ) )
36	35	spvv	⊢ ( ∀ 𝑥 ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
37	24 36	sylbi	⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
38		simpl	⊢ ( ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝑧 ≈ 𝐵 )
39	37 38	syl6bi	⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝑧 ≈ 𝐵 ) )
40	21 39	jcad	⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → ( 𝑧 ≈ 𝐴 ∧ 𝑧 ≈ 𝐵 ) ) )
41		ensym	⊢ ( 𝑧 ≈ 𝐴 → 𝐴 ≈ 𝑧 )
42		entr	⊢ ( ( 𝐴 ≈ 𝑧 ∧ 𝑧 ≈ 𝐵 ) → 𝐴 ≈ 𝐵 )
43	41 42	sylan	⊢ ( ( 𝑧 ≈ 𝐴 ∧ 𝑧 ≈ 𝐵 ) → 𝐴 ≈ 𝐵 )
44	40 43	syl6	⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝐴 ≈ 𝐵 ) )
45	19 44	syl5bi	⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) → 𝐴 ≈ 𝐵 ) )
46	45	expd	⊢ ( 𝐶 = 𝐷 → ( 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } → ( ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) → 𝐴 ≈ 𝐵 ) ) )
47	46	rexlimdv	⊢ ( 𝐶 = 𝐷 → ( ∃ 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) → 𝐴 ≈ 𝐵 ) )
48	13 47	mpi	⊢ ( 𝐶 = 𝐷 → 𝐴 ≈ 𝐵 )
49		enen2	⊢ ( 𝐴 ≈ 𝐵 → ( 𝑥 ≈ 𝐴 ↔ 𝑥 ≈ 𝐵 ) )
50		enen2	⊢ ( 𝐴 ≈ 𝐵 → ( 𝑦 ≈ 𝐴 ↔ 𝑦 ≈ 𝐵 ) )
51	50	imbi1d	⊢ ( 𝐴 ≈ 𝐵 → ( ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
52	51	albidv	⊢ ( 𝐴 ≈ 𝐵 → ( ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
53	49 52	anbi12d	⊢ ( 𝐴 ≈ 𝐵 → ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
54	53	abbidv	⊢ ( 𝐴 ≈ 𝐵 → { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } )
55	54 2 3	3eqtr4g	⊢ ( 𝐴 ≈ 𝐵 → 𝐶 = 𝐷 )
56	48 55	impbii	⊢ ( 𝐶 = 𝐷 ↔ 𝐴 ≈ 𝐵 )