Theorem kardexen

Description: One set is equinumerous to another iff an element in its kard cardinality is equinumerous to an element in the second set's kard cardinality. See kardeng for a version with equality of cardinals. (Contributed by BTernaryTau, 7-Jul-2026)

	Ref	Expression
Assertion	kardexen	Could not format assertion : No typesetting found for |- ( A ~~ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		2r19.29	Could not format ( ( A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y /\ E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y ) -> E. x e. ( kard ` A ) E. y e. ( kard ` B ) ( -. x ~< y /\ x ~<_ y ) ) : No typesetting found for |- ( ( A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y /\ E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y ) -> E. x e. ( kard ` A ) E. y e. ( kard ` B ) ( -. x ~< y /\ x ~<_ y ) ) with typecode |-
2		bren2	$$⊢A\approx B\leftrightarrow \left(A\preccurlyeq B\wedge \neg A\prec B\right)$$
3		kardsdom	Could not format ( A ~< B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y ) : No typesetting found for |- ( A ~< B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y ) with typecode |-
4	3	notbii	Could not format ( -. A ~< B <-> -. E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y ) : No typesetting found for |- ( -. A ~< B <-> -. E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y ) with typecode |-
5		ralnex2	Could not format ( A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y <-> -. E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y ) : No typesetting found for |- ( A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y <-> -. E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y ) with typecode |-
6	4 5	bitr4i	Could not format ( -. A ~< B <-> A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) : No typesetting found for |- ( -. A ~< B <-> A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) with typecode |-
7	6	anbi2i	Could not format ( ( A ~<_ B /\ -. A ~< B ) <-> ( A ~<_ B /\ A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) ) : No typesetting found for |- ( ( A ~<_ B /\ -. A ~< B ) <-> ( A ~<_ B /\ A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) ) with typecode |-
8	2 7	bitri	Could not format ( A ~~ B <-> ( A ~<_ B /\ A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) ) : No typesetting found for |- ( A ~~ B <-> ( A ~<_ B /\ A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) ) with typecode |-
9		karddom	Could not format ( A ~<_ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y ) : No typesetting found for |- ( A ~<_ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y ) with typecode |-
10	8 9	bianbi	Could not format ( A ~~ B <-> ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y /\ A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) ) : No typesetting found for |- ( A ~~ B <-> ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y /\ A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) ) with typecode |-
11	10	biancomi	Could not format ( A ~~ B <-> ( A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y /\ E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y ) ) : No typesetting found for |- ( A ~~ B <-> ( A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y /\ E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y ) ) with typecode |-
12		bren2	$$⊢x\approx y\leftrightarrow \left(x\preccurlyeq y\wedge \neg x\prec y\right)$$
13	12	biancomi	$$⊢x\approx y\leftrightarrow \left(\neg x\prec y\wedge x\preccurlyeq y\right)$$
14	13	2rexbii	Could not format ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) ( -. x ~< y /\ x ~<_ y ) ) : No typesetting found for |- ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) ( -. x ~< y /\ x ~<_ y ) ) with typecode |-
15	1 11 14	3imtr4i	Could not format ( A ~~ B -> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y ) : No typesetting found for |- ( A ~~ B -> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y ) with typecode |-
16		elkarden	Could not format ( x e. ( kard ` A ) -> x ~~ A ) : No typesetting found for |- ( x e. ( kard ` A ) -> x ~~ A ) with typecode |-
17		elkarden	Could not format ( y e. ( kard ` B ) -> y ~~ B ) : No typesetting found for |- ( y e. ( kard ` B ) -> y ~~ B ) with typecode |-
18		ensym	$$⊢x\approx A\to A\approx x$$
19		entr	$$⊢\left(A\approx x\wedge x\approx y\right)\to A\approx y$$
20	18 19	sylan	$$⊢\left(x\approx A\wedge x\approx y\right)\to A\approx y$$
21	20	ancoms	$$⊢\left(x\approx y\wedge x\approx A\right)\to A\approx y$$
22		entr	$$⊢\left(A\approx y\wedge y\approx B\right)\to A\approx B$$
23	21 22	stoic3	$$⊢\left(x\approx y\wedge x\approx A\wedge y\approx B\right)\to A\approx B$$
24	23	3expib	$$⊢x\approx y\to \left(\left(x\approx A\wedge y\approx B\right)\to A\approx B\right)$$
25	24	com12	$$⊢\left(x\approx A\wedge y\approx B\right)\to \left(x\approx y\to A\approx B\right)$$
26	16 17 25	syl2an	Could not format ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> ( x ~~ y -> A ~~ B ) ) : No typesetting found for |- ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> ( x ~~ y -> A ~~ B ) ) with typecode |-
27	26	rexlimivv	Could not format ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y -> A ~~ B ) : No typesetting found for |- ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y -> A ~~ B ) with typecode |-
28	15 27	impbii	Could not format ( A ~~ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y ) : No typesetting found for |- ( A ~~ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y ) with typecode |-