Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 2r19.29 ⊢ ( ( ∀ 𝑥 ∈ ( kard ‘ 𝐴 ) ∀ 𝑦 ∈ ( kard ‘ 𝐵 ) ¬ 𝑥 ≺ 𝑦 ∧ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ) → ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) ( ¬ 𝑥 ≺ 𝑦 ∧ 𝑥 ≼ 𝑦 ) )
2 bren2 ⊢ ( 𝐴 ≈ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵 ) )
3 kardsdom ⊢ ( 𝐴 ≺ 𝐵 ↔ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≺ 𝑦 )
4 3 notbii ⊢ ( ¬ 𝐴 ≺ 𝐵 ↔ ¬ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≺ 𝑦 )
5 ralnex2 ⊢ ( ∀ 𝑥 ∈ ( kard ‘ 𝐴 ) ∀ 𝑦 ∈ ( kard ‘ 𝐵 ) ¬ 𝑥 ≺ 𝑦 ↔ ¬ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≺ 𝑦 )
6 4 5 bitr4i ⊢ ( ¬ 𝐴 ≺ 𝐵 ↔ ∀ 𝑥 ∈ ( kard ‘ 𝐴 ) ∀ 𝑦 ∈ ( kard ‘ 𝐵 ) ¬ 𝑥 ≺ 𝑦 )
7 6 anbi2i ⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵 ) ↔ ( 𝐴 ≼ 𝐵 ∧ ∀ 𝑥 ∈ ( kard ‘ 𝐴 ) ∀ 𝑦 ∈ ( kard ‘ 𝐵 ) ¬ 𝑥 ≺ 𝑦 ) )
8 2 7 bitri ⊢ ( 𝐴 ≈ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ∀ 𝑥 ∈ ( kard ‘ 𝐴 ) ∀ 𝑦 ∈ ( kard ‘ 𝐵 ) ¬ 𝑥 ≺ 𝑦 ) )
9 karddom ⊢ ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 )
10 8 9 bianbi ⊢ ( 𝐴 ≈ 𝐵 ↔ ( ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ∧ ∀ 𝑥 ∈ ( kard ‘ 𝐴 ) ∀ 𝑦 ∈ ( kard ‘ 𝐵 ) ¬ 𝑥 ≺ 𝑦 ) )
11 10 biancomi ⊢ ( 𝐴 ≈ 𝐵 ↔ ( ∀ 𝑥 ∈ ( kard ‘ 𝐴 ) ∀ 𝑦 ∈ ( kard ‘ 𝐵 ) ¬ 𝑥 ≺ 𝑦 ∧ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≼ 𝑦 ) )
12 bren2 ⊢ ( 𝑥 ≈ 𝑦 ↔ ( 𝑥 ≼ 𝑦 ∧ ¬ 𝑥 ≺ 𝑦 ) )
13 12 biancomi ⊢ ( 𝑥 ≈ 𝑦 ↔ ( ¬ 𝑥 ≺ 𝑦 ∧ 𝑥 ≼ 𝑦 ) )
14 13 2rexbii ⊢ ( ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≈ 𝑦 ↔ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) ( ¬ 𝑥 ≺ 𝑦 ∧ 𝑥 ≼ 𝑦 ) )
15 1 11 14 3imtr4i ⊢ ( 𝐴 ≈ 𝐵 → ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≈ 𝑦 )
16 elkarden ⊢ ( 𝑥 ∈ ( kard ‘ 𝐴 ) → 𝑥 ≈ 𝐴 )
17 elkarden ⊢ ( 𝑦 ∈ ( kard ‘ 𝐵 ) → 𝑦 ≈ 𝐵 )
18 ensym ⊢ ( 𝑥 ≈ 𝐴 → 𝐴 ≈ 𝑥 )
19 entr ⊢ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ≈ 𝑦 ) → 𝐴 ≈ 𝑦 )
20 18 19 sylan ⊢ ( ( 𝑥 ≈ 𝐴 ∧ 𝑥 ≈ 𝑦 ) → 𝐴 ≈ 𝑦 )
21 20 ancoms ⊢ ( ( 𝑥 ≈ 𝑦 ∧ 𝑥 ≈ 𝐴 ) → 𝐴 ≈ 𝑦 )
22 entr ⊢ ( ( 𝐴 ≈ 𝑦 ∧ 𝑦 ≈ 𝐵 ) → 𝐴 ≈ 𝐵 )
23 21 22 stoic3 ⊢ ( ( 𝑥 ≈ 𝑦 ∧ 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → 𝐴 ≈ 𝐵 )
24 23 3expib ⊢ ( 𝑥 ≈ 𝑦 → ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → 𝐴 ≈ 𝐵 ) )
25 24 com12 ⊢ ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) → ( 𝑥 ≈ 𝑦 → 𝐴 ≈ 𝐵 ) )
26 16 17 25 syl2an ⊢ ( ( 𝑥 ∈ ( kard ‘ 𝐴 ) ∧ 𝑦 ∈ ( kard ‘ 𝐵 ) ) → ( 𝑥 ≈ 𝑦 → 𝐴 ≈ 𝐵 ) )
27 26 rexlimivv ⊢ ( ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≈ 𝑦 → 𝐴 ≈ 𝐵 )
28 15 27 impbii ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑥 ∈ ( kard ‘ 𝐴 ) ∃ 𝑦 ∈ ( kard ‘ 𝐵 ) 𝑥 ≈ 𝑦 )