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	⊢ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ )