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	⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2	1	brrelex1i	⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
3		kardeq0	⊢ ( ( kard ‘ 𝐴 ) = ∅ ↔ ¬ 𝐴 ∈ V )
4	3	necon2abii	⊢ ( 𝐴 ∈ V ↔ ( kard ‘ 𝐴 ) ≠ ∅ )
5	2 4	sylib	⊢ ( 𝐴 ≼ 𝐵 → ( kard ‘ 𝐴 ) ≠ ∅ )
6		n0	⊢ ( ( kard ‘ 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( kard ‘ 𝐴 ) )
7	5 6	sylib	⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑥 𝑥 ∈ ( kard ‘ 𝐴 ) )
8	1	brrelex2i	⊢ ( 𝐴 ≼ 𝐵 → 𝐵 ∈ V )
9		kardeq0	⊢ ( ( kard ‘ 𝐵 ) = ∅ ↔ ¬ 𝐵 ∈ V )
10	9	necon2abii	⊢ ( 𝐵 ∈ V ↔ ( kard ‘ 𝐵 ) ≠ ∅ )
11	8 10	sylib	⊢ ( 𝐴 ≼ 𝐵 → ( kard ‘ 𝐵 ) ≠ ∅ )
12		n0	⊢ ( ( kard ‘ 𝐵 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( kard ‘ 𝐵 ) )
13	11 12	sylib	⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑦 𝑦 ∈ ( kard ‘ 𝐵 ) )
14		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ 𝑦 ∈ ( kard ‘ 𝐵 ) ) ↔ ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ ∃ 𝑦 𝑦 ∈ ( kard ‘ 𝐵 ) ) )
15		simpr	⊢ ( ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ 𝑦 ∈ ( kard ‘ 𝐵 ) ) → 𝑦 ∈ ( kard ‘ 𝐵 ) )
16	15	a1i	⊢ ( 𝐴 ≼ 𝐵 → ( ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ 𝑦 ∈ ( kard ‘ 𝐵 ) ) → 𝑦 ∈ ( kard ‘ 𝐵 ) ) )
17		elkarden	⊢ ( 𝑥 ∈ ( kard ‘ 𝐴 ) → 𝑥 ≈ 𝐴 )
18		elkarden	⊢ ( 𝑦 ∈ ( kard ‘ 𝐵 ) → 𝑦 ≈ 𝐵 )
19		endomtr	⊢ ( ( 𝑥 ≈ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → 𝑥 ≼ 𝐵 )
20	19	ancoms	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝑥 ≈ 𝐴 ) → 𝑥 ≼ 𝐵 )
21		ensym	⊢ ( 𝑦 ≈ 𝐵 → 𝐵 ≈ 𝑦 )
22		domentr	⊢ ( ( 𝑥 ≼ 𝐵 ∧ 𝐵 ≈ 𝑦 ) → 𝑥 ≼ 𝑦 )
23	21 22	sylan2	⊢ ( ( 𝑥 ≼ 𝐵 ∧ 𝑦 ≈ 𝐵 ) → 𝑥 ≼ 𝑦 )
24	20 23	stoic3	⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → 𝑥 ≼ 𝑦 )
25	24	3expib	⊢ ( 𝐴 ≼ 𝐵 → ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → 𝑥 ≼ 𝑦 ) )
26	17 18 25	syl2ani	⊢ ( 𝐴 ≼ 𝐵 → ( ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ 𝑦 ∈ ( kard ‘ 𝐵 ) ) → 𝑥 ≼ 𝑦 ) )
27	16 26	jcad	⊢ ( 𝐴 ≼ 𝐵 → ( ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ 𝑦 ∈ ( kard ‘ 𝐵 ) ) → ( 𝑦 ∈ ( kard ‘ 𝐵 ) ∧ 𝑥 ≼ 𝑦 ) ) )
28	27	eximdv	⊢ ( 𝐴 ≼ 𝐵 → ( ∃ 𝑦 ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ 𝑦 ∈ ( kard ‘ 𝐵 ) ) → ∃ 𝑦 ( 𝑦 ∈ ( kard ‘ 𝐵 ) ∧ 𝑥 ≼ 𝑦 ) ) )
29	14 28	biimtrrid	⊢ ( 𝐴 ≼ 𝐵 → ( ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ ∃ 𝑦 𝑦 ∈ ( kard ‘ 𝐵 ) ) → ∃ 𝑦 ( 𝑦 ∈ ( kard ‘ 𝐵 ) ∧ 𝑥 ≼ 𝑦 ) ) )
30	13 29	mpan2d	⊢ ( 𝐴 ≼ 𝐵 → ( 𝑥 ∈ ( kard ‘ 𝐴 ) → ∃ 𝑦 ( 𝑦 ∈ ( kard ‘ 𝐵 ) ∧ 𝑥 ≼ 𝑦 ) ) )
31		df-rex	⊢ ( ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ ( kard ‘ 𝐵 ) ∧ 𝑥 ≼ 𝑦 ) )
32	30 31	imbitrrdi	⊢ ( 𝐴 ≼ 𝐵 → ( 𝑥 ∈ ( kard ‘ 𝐴 ) → ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ) )
33	32	ancld	⊢ ( 𝐴 ≼ 𝐵 → ( 𝑥 ∈ ( kard ‘ 𝐴 ) → ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ) ) )
34	33	eximdv	⊢ ( 𝐴 ≼ 𝐵 → ( ∃ 𝑥 𝑥 ∈ ( kard ‘ 𝐴 ) → ∃ 𝑥 ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ) ) )
35	7 34	mpd	⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑥 ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ) )
36		df-rex	⊢ ( ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ) )
37	35 36	sylibr	⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 )
38		ensym	⊢ ( 𝑥 ≈ 𝐴 → 𝐴 ≈ 𝑥 )
39		endomtr	⊢ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ≼ 𝑦 ) → 𝐴 ≼ 𝑦 )
40	38 39	sylan	⊢ ( ( 𝑥 ≈ 𝐴 ∧ 𝑥 ≼ 𝑦 ) → 𝐴 ≼ 𝑦 )
41	40	ancoms	⊢ ( ( 𝑥 ≼ 𝑦 ∧ 𝑥 ≈ 𝐴 ) → 𝐴 ≼ 𝑦 )
42		domentr	⊢ ( ( 𝐴 ≼ 𝑦 ∧ 𝑦 ≈ 𝐵 ) → 𝐴 ≼ 𝐵 )
43	41 42	stoic3	⊢ ( ( 𝑥 ≼ 𝑦 ∧ 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → 𝐴 ≼ 𝐵 )
44	43	3expib	⊢ ( 𝑥 ≼ 𝑦 → ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → 𝐴 ≼ 𝐵 ) )
45	44	com12	⊢ ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → ( 𝑥 ≼ 𝑦 → 𝐴 ≼ 𝐵 ) )
46	17 18 45	syl2an	⊢ ( ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ 𝑦 ∈ ( kard ‘ 𝐵 ) ) → ( 𝑥 ≼ 𝑦 → 𝐴 ≼ 𝐵 ) )
47	46	rexlimivv	⊢ ( ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 → 𝐴 ≼ 𝐵 )
48	37 47	impbii	⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 )