Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex1i 
 |-  ( A ~<_ B -> A e. _V )
3 kardeq0 
 |-  ( ( kard ` A ) = (/) <-> -. A e. _V )
4 3 necon2abii 
 |-  ( A e. _V <-> ( kard ` A ) =/= (/) )
5 2 4 sylib 
 |-  ( A ~<_ B -> ( kard ` A ) =/= (/) )
6 n0 
 |-  ( ( kard ` A ) =/= (/) <-> E. x x e. ( kard ` A ) )
7 5 6 sylib 
 |-  ( A ~<_ B -> E. x x e. ( kard ` A ) )
8 1 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
9 kardeq0 
 |-  ( ( kard ` B ) = (/) <-> -. B e. _V )
10 9 necon2abii 
 |-  ( B e. _V <-> ( kard ` B ) =/= (/) )
11 8 10 sylib 
 |-  ( A ~<_ B -> ( kard ` B ) =/= (/) )
12 n0 
 |-  ( ( kard ` B ) =/= (/) <-> E. y y e. ( kard ` B ) )
13 11 12 sylib 
 |-  ( A ~<_ B -> E. y y e. ( kard ` B ) )
14 19.42v 
 |-  ( E. y ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) <-> ( x e. ( kard ` A ) /\ E. y y e. ( kard ` B ) ) )
15 simpr 
 |-  ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> y e. ( kard ` B ) )
16 15 a1i 
 |-  ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> y e. ( kard ` B ) ) )
17 elkarden 
 |-  ( x e. ( kard ` A ) -> x ~~ A )
18 elkarden 
 |-  ( y e. ( kard ` B ) -> y ~~ B )
19 endomtr 
 |-  ( ( x ~~ A /\ A ~<_ B ) -> x ~<_ B )
20 19 ancoms 
 |-  ( ( A ~<_ B /\ x ~~ A ) -> x ~<_ B )
21 ensym 
 |-  ( y ~~ B -> B ~~ y )
22 domentr 
 |-  ( ( x ~<_ B /\ B ~~ y ) -> x ~<_ y )
23 21 22 sylan2 
 |-  ( ( x ~<_ B /\ y ~~ B ) -> x ~<_ y )
24 20 23 stoic3 
 |-  ( ( A ~<_ B /\ x ~~ A /\ y ~~ B ) -> x ~<_ y )
25 24 3expib 
 |-  ( A ~<_ B -> ( ( x ~~ A /\ y ~~ B ) -> x ~<_ y ) )
26 17 18 25 syl2ani 
 |-  ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> x ~<_ y ) )
27 16 26 jcad 
 |-  ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> ( y e. ( kard ` B ) /\ x ~<_ y ) ) )
28 27 eximdv 
 |-  ( A ~<_ B -> ( E. y ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) )
29 14 28 biimtrrid 
 |-  ( A ~<_ B -> ( ( x e. ( kard ` A ) /\ E. y y e. ( kard ` B ) ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) )
30 13 29 mpan2d 
 |-  ( A ~<_ B -> ( x e. ( kard ` A ) -> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) ) )
31 df-rex 
 |-  ( E. y e. ( kard ` B ) x ~<_ y <-> E. y ( y e. ( kard ` B ) /\ x ~<_ y ) )
32 30 31 imbitrrdi 
 |-  ( A ~<_ B -> ( x e. ( kard ` A ) -> E. y e. ( kard ` B ) x ~<_ y ) )
33 32 ancld 
 |-  ( A ~<_ B -> ( x e. ( kard ` A ) -> ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) )
34 33 eximdv 
 |-  ( A ~<_ B -> ( E. x x e. ( kard ` A ) -> E. x ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) ) )
35 7 34 mpd 
 |-  ( A ~<_ B -> E. x ( x e. ( kard ` A ) /\ E. y e. ( kard ` B ) x ~<_ y ) )
36 df-rex 
 |-  ( 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 ) )
37 35 36 sylibr 
 |-  ( A ~<_ B -> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y )
38 ensym 
 |-  ( x ~~ A -> A ~~ x )
39 endomtr 
 |-  ( ( A ~~ x /\ x ~<_ y ) -> A ~<_ y )
40 38 39 sylan 
 |-  ( ( x ~~ A /\ x ~<_ y ) -> A ~<_ y )
41 40 ancoms 
 |-  ( ( x ~<_ y /\ x ~~ A ) -> A ~<_ y )
42 domentr 
 |-  ( ( A ~<_ y /\ y ~~ B ) -> A ~<_ B )
43 41 42 stoic3 
 |-  ( ( x ~<_ y /\ x ~~ A /\ y ~~ B ) -> A ~<_ B )
44 43 3expib 
 |-  ( x ~<_ y -> ( ( x ~~ A /\ y ~~ B ) -> A ~<_ B ) )
45 44 com12 
 |-  ( ( x ~~ A /\ y ~~ B ) -> ( x ~<_ y -> A ~<_ B ) )
46 17 18 45 syl2an 
 |-  ( ( x e. ( kard ` A ) /\ y e. ( kard ` B ) ) -> ( x ~<_ y -> A ~<_ B ) )
47 46 rexlimivv 
 |-  ( E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y -> A ~<_ B )
48 37 47 impbii 
 |-  ( A ~<_ B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~<_ y )