Theorem karddom

Description: One set dominates another iff an element in its kard cardinality dominates an element in the second set's kard cardinality. (Contributed by BTernaryTau, 4-Jul-2026)

	Ref	Expression
Assertion	karddom	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		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
2	1	brrelex1i	$$⊢A\preccurlyeq B\to A\in \mathrm{V}$$
3		kardeq0	Could not format ( ( kard ` A ) = (/) <-> -. A e. _V ) : No typesetting found for |- ( ( kard ` A ) = (/) <-> -. A e. _V ) with typecode |-
4	3	necon2abii	Could not format ( A e. _V <-> ( kard ` A ) =/= (/) ) : No typesetting found for |- ( A e. _V <-> ( kard ` A ) =/= (/) ) with typecode |-
5	2 4	sylib	Could not format ( A ~<_ B -> ( kard ` A ) =/= (/) ) : No typesetting found for |- ( A ~<_ B -> ( kard ` A ) =/= (/) ) with typecode |-
6		n0	Could not format ( ( kard ` A ) =/= (/) <-> E. x x e. ( kard ` A ) ) : No typesetting found for |- ( ( kard ` A ) =/= (/) <-> E. x x e. ( kard ` A ) ) with typecode |-
7	5 6	sylib	Could not format ( A ~<_ B -> E. x x e. ( kard ` A ) ) : No typesetting found for |- ( A ~<_ B -> E. x x e. ( kard ` A ) ) with typecode |-
8	1	brrelex2i	$$⊢A\preccurlyeq B\to B\in \mathrm{V}$$
9		kardeq0	Could not format ( ( kard ` B ) = (/) <-> -. B e. _V ) : No typesetting found for |- ( ( kard ` B ) = (/) <-> -. B e. _V ) with typecode |-
10	9	necon2abii	Could not format ( B e. _V <-> ( kard ` B ) =/= (/) ) : No typesetting found for |- ( B e. _V <-> ( kard ` B ) =/= (/) ) with typecode |-
11	8 10	sylib	Could not format ( A ~<_ B -> ( kard ` B ) =/= (/) ) : No typesetting found for |- ( A ~<_ B -> ( kard ` B ) =/= (/) ) with typecode |-
12		n0	Could not format ( ( kard ` B ) =/= (/) <-> E. y y e. ( kard ` B ) ) : No typesetting found for |- ( ( kard ` B ) =/= (/) <-> E. y y e. ( kard ` B ) ) with typecode |-
13	11 12	sylib	Could not format ( A ~<_ B -> E. y y e. ( kard ` B ) ) : No typesetting found for |- ( A ~<_ B -> E. y y e. ( kard ` B ) ) with typecode |-
14		19.42v	Could not format ( E. y ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) <-> ( x e. ( kard ` A ) /\ E. y y e. ( kard ` B ) ) ) : No typesetting found for |- ( E. y ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) <-> ( x e. ( kard ` A ) /\ E. y y e. ( kard ` B ) ) ) with typecode |-
15		simpr	Could not format ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> y e. ( kard ` B ) ) : No typesetting found for |- ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> y e. ( kard ` B ) ) with typecode |-
16	15	a1i	Could not format ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> y e. ( kard ` B ) ) ) : No typesetting found for |- ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> y e. ( kard ` B ) ) ) with typecode |-
17		elkarden	Could not format ( x e. ( kard ` A ) -> x ~~ A ) : No typesetting found for |- ( x e. ( kard ` A ) -> x ~~ A ) with typecode |-
18		elkarden	Could not format ( y e. ( kard ` B ) -> y ~~ B ) : No typesetting found for |- ( y e. ( kard ` B ) -> y ~~ B ) with typecode |-
19		endomtr	$$⊢\left(x\approx A\wedge A\preccurlyeq B\right)\to x\preccurlyeq B$$
20	19	ancoms	$$⊢\left(A\preccurlyeq B\wedge x\approx A\right)\to x\preccurlyeq B$$
21		ensym	$$⊢y\approx B\to B\approx y$$
22		domentr	$$⊢\left(x\preccurlyeq B\wedge B\approx y\right)\to x\preccurlyeq y$$
23	21 22	sylan2	$$⊢\left(x\preccurlyeq B\wedge y\approx B\right)\to x\preccurlyeq y$$
24	20 23	stoic3	$$⊢\left(A\preccurlyeq B\wedge x\approx A\wedge y\approx B\right)\to x\preccurlyeq y$$
25	24	3expib	$$⊢A\preccurlyeq B\to \left(\left(x\approx A\wedge y\approx B\right)\to x\preccurlyeq y\right)$$
26	17 18 25	syl2ani	Could not format ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> x ~<_ y ) ) : No typesetting found for |- ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> x ~<_ y ) ) with typecode |-
27	16 26	jcad	Could not format ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> ( y e. ( kard ` B ) /\ x ~<_ y ) ) ) : No typesetting found for |- ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> ( y e. ( kard ` B ) /\ x ~<_ y ) ) ) with typecode |-
28	27	eximdv	Could not format ( A ~<_ B -> ( E. y ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) ) : No typesetting found for |- ( A ~<_ B -> ( E. y ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) ) with typecode |-
29	14 28	biimtrrid	Could not format ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ E. y y e. ( kard ` B ) ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) ) : No typesetting found for |- ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ E. y y e. ( kard ` B ) ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) ) with typecode |-
30	13 29	mpan2d	Could not format ( A ~<_ B -> ( x e. ( kard ` A ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) ) : No typesetting found for |- ( A ~<_ B -> ( x e. ( kard ` A ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) ) with typecode |-
31		df-rex	Could not format ( E. y e. ( kard ` B ) x ~<_ y <-> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) : No typesetting found for |- ( E. y e. ( kard ` B ) x ~<_ y <-> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) with typecode |-
32	30 31	imbitrrdi	Could not format ( A ~<_ B -> ( x e. ( kard ` A ) -> E. y e. ( kard ` B ) x ~<_ y ) ) : No typesetting found for |- ( A ~<_ B -> ( x e. ( kard ` A ) -> E. y e. ( kard ` B ) x ~<_ y ) ) with typecode |-
33	32	ancld	Could not format ( A ~<_ B -> ( x e. ( kard ` A ) -> ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) ) : No typesetting found for |- ( A ~<_ B -> ( x e. ( kard ` A ) -> ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) ) with typecode |-
34	33	eximdv	Could not format ( A ~<_ B -> ( E. x x e. ( kard ` A ) -> E. x ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) ) : No typesetting found for |- ( A ~<_ B -> ( E. x x e. ( kard ` A ) -> E. x ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) ) with typecode |-
35	7 34	mpd	Could not format ( A ~<_ B -> E. x ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) : No typesetting found for |- ( A ~<_ B -> E. x ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) with typecode |-
36		df-rex	Could not format ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y <-> E. x ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) : No typesetting found for |- ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y <-> E. x ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) with typecode |-
37	35 36	sylibr	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 |-
38		ensym	$$⊢x\approx A\to A\approx x$$
39		endomtr	$$⊢\left(A\approx x\wedge x\preccurlyeq y\right)\to A\preccurlyeq y$$
40	38 39	sylan	$$⊢\left(x\approx A\wedge x\preccurlyeq y\right)\to A\preccurlyeq y$$
41	40	ancoms	$$⊢\left(x\preccurlyeq y\wedge x\approx A\right)\to A\preccurlyeq y$$
42		domentr	$$⊢\left(A\preccurlyeq y\wedge y\approx B\right)\to A\preccurlyeq B$$
43	41 42	stoic3	$$⊢\left(x\preccurlyeq y\wedge x\approx A\wedge y\approx B\right)\to A\preccurlyeq B$$
44	43	3expib	$$⊢x\preccurlyeq y\to \left(\left(x\approx A\wedge y\approx B\right)\to A\preccurlyeq B\right)$$
45	44	com12	$$⊢\left(x\approx A\wedge y\approx B\right)\to \left(x\preccurlyeq y\to A\preccurlyeq B\right)$$
46	17 18 45	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 |-
47	46	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 |-
48	37 47	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 |-