This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem endisj

Description: Any two sets are equinumerous to two disjoint sets. Exercise 4.39 of Mendelson p. 255. (Contributed by NM, 16-Apr-2004)

Ref Expression
Hypotheses endisj.1 ⊢ 𝐴 ∈ V
endisj.2 ⊢ 𝐵 ∈ V
Assertion endisj ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ )

Proof

Step Hyp Ref Expression
1 endisj.1 ⊢ 𝐴 ∈ V
2 endisj.2 ⊢ 𝐵 ∈ V
3 0ex ⊢ ∅ ∈ V
4 1 3 xpsnen ⊢ ( 𝐴 × { ∅ } ) ≈ 𝐴
5 1oex ⊢ 1o ∈ V
6 2 5 xpsnen ⊢ ( 𝐵 × { 1o } ) ≈ 𝐵
7 4 6 pm3.2i ⊢ ( ( 𝐴 × { ∅ } ) ≈ 𝐴 ∧ ( 𝐵 × { 1o } ) ≈ 𝐵 )
8 xp01disj ⊢ ( ( 𝐴 × { ∅ } ) ∩ ( 𝐵 × { 1o } ) ) = ∅
9 p0ex ⊢ { ∅ } ∈ V
10 1 9 xpex ⊢ ( 𝐴 × { ∅ } ) ∈ V
11 snex ⊢ { 1o } ∈ V
12 2 11 xpex ⊢ ( 𝐵 × { 1o } ) ∈ V
13 breq1 ⊢ ( 𝑥 = ( 𝐴 × { ∅ } ) → ( 𝑥 ≈ 𝐴 ↔ ( 𝐴 × { ∅ } ) ≈ 𝐴 ) )
14 breq1 ⊢ ( 𝑦 = ( 𝐵 × { 1o } ) → ( 𝑦 ≈ 𝐵 ↔ ( 𝐵 × { 1o } ) ≈ 𝐵 ) )
15 13 14 bi2anan9 ⊢ ( ( 𝑥 = ( 𝐴 × { ∅ } ) ∧ 𝑦 = ( 𝐵 × { 1o } ) ) → ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ↔ ( ( 𝐴 × { ∅ } ) ≈ 𝐴 ∧ ( 𝐵 × { 1o } ) ≈ 𝐵 ) ) )
16 ineq12 ⊢ ( ( 𝑥 = ( 𝐴 × { ∅ } ) ∧ 𝑦 = ( 𝐵 × { 1o } ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝐴 × { ∅ } ) ∩ ( 𝐵 × { 1o } ) ) )
17 16 eqeq1d ⊢ ( ( 𝑥 = ( 𝐴 × { ∅ } ) ∧ 𝑦 = ( 𝐵 × { 1o } ) ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ( ( 𝐴 × { ∅ } ) ∩ ( 𝐵 × { 1o } ) ) = ∅ ) )
18 15 17 anbi12d ⊢ ( ( 𝑥 = ( 𝐴 × { ∅ } ) ∧ 𝑦 = ( 𝐵 × { 1o } ) ) → ( ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝐴 × { ∅ } ) ≈ 𝐴 ∧ ( 𝐵 × { 1o } ) ≈ 𝐵 ) ∧ ( ( 𝐴 × { ∅ } ) ∩ ( 𝐵 × { 1o } ) ) = ∅ ) ) )
19 10 12 18 spc2ev ⊢ ( ( ( ( 𝐴 × { ∅ } ) ≈ 𝐴 ∧ ( 𝐵 × { 1o } ) ≈ 𝐵 ) ∧ ( ( 𝐴 × { ∅ } ) ∩ ( 𝐵 × { 1o } ) ) = ∅ ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
20 7 8 19 mp2an ⊢ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ )