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	|- ( A ~~ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y )

Proof

Step	Hyp	Ref	Expression
1		2r19.29	|- ( ( 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 ) )
2		bren2	|- ( A ~~ B <-> ( A ~<_ B /\ -. A ~< B ) )
3		kardsdom	|- ( A ~< B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y )
4	3	notbii	|- ( -. A ~< B <-> -. E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y )
5		ralnex2	|- ( A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y <-> -. E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y )
6	4 5	bitr4i	|- ( -. A ~< B <-> A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y )
7	6	anbi2i	|- ( ( A ~<_ B /\ -. A ~< B ) <-> ( A ~<_ B /\ A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) )
8	2 7	bitri	|- ( A ~~ B <-> ( A ~<_ B /\ A. x e. ( kard ` A ) A. y e. ( kard ` B ) -. x ~< y ) )
9		karddom	|- ( A ~<_ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y )
10	8 9	bianbi	|- ( 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 ) )
11	10	biancomi	|- ( 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 ) )
12		bren2	|- ( x ~~ y <-> ( x ~<_ y /\ -. x ~< y ) )
13	12	biancomi	|- ( x ~~ y <-> ( -. x ~< y /\ x ~<_ y ) )
14	13	2rexbii	|- ( 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 ) )
15	1 11 14	3imtr4i	|- ( A ~~ B -> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y )
16		elkarden	|- ( x e. ( kard ` A ) -> x ~~ A )
17		elkarden	|- ( y e. ( kard ` B ) -> y ~~ B )
18		ensym	|- ( x ~~ A -> A ~~ x )
19		entr	|- ( ( A ~~ x /\ x ~~ y ) -> A ~~ y )
20	18 19	sylan	|- ( ( x ~~ A /\ x ~~ y ) -> A ~~ y )
21	20	ancoms	|- ( ( x ~~ y /\ x ~~ A ) -> A ~~ y )
22		entr	|- ( ( A ~~ y /\ y ~~ B ) -> A ~~ B )
23	21 22	stoic3	|- ( ( x ~~ y /\ x ~~ A /\ y ~~ B ) -> A ~~ B )
24	23	3expib	|- ( x ~~ y -> ( ( x ~~ A /\ y ~~ B ) -> A ~~ B ) )
25	24	com12	|- ( ( x ~~ A /\ y ~~ B ) -> ( x ~~ y -> A ~~ B ) )
26	16 17 25	syl2an	|- ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> ( x ~~ y -> A ~~ B ) )
27	26	rexlimivv	|- ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y -> A ~~ B )
28	15 27	impbii	|- ( A ~~ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~~ y )