Metamath Proof Explorer

Theorem kardsdom

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

Ref Expression
Assertion kardsdom 
|- ( A ~< B <-> E. x e. ( kard ` A ) E. y e. ( kard ` B ) x ~< y )

Proof

Step Hyp Ref Expression
1 relsdom 
 |-  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 ensdomtr 
 |-  ( ( x ~~ A /\ A ~< B ) -> x ~< B )
20 19 ancoms 
 |-  ( ( A ~< B /\ x ~~ A ) -> x ~< B )
21 ensym 
 |-  ( y ~~ B -> B ~~ y )
22 sdomentr 
 |-  ( ( 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 ensdomtr 
 |-  ( ( 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 sdomentr 
 |-  ( ( 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 )