Theorem infdju1

Description: An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	infdju1	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		difun2	⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ ( { 1o } × 1o ) ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) )
2		df-dju	⊢ ( 𝐴 ⊔ 1o ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
3		df1o2	⊢ 1o = { ∅ }
4	3	xpeq2i	⊢ ( { 1o } × 1o ) = ( { 1o } × { ∅ } )
5		1oex	⊢ 1o ∈ V
6		0ex	⊢ ∅ ∈ V
7	5 6	xpsn	⊢ ( { 1o } × { ∅ } ) = { ⟨ 1o , ∅ ⟩ }
8	4 7	eqtr2i	⊢ { ⟨ 1o , ∅ ⟩ } = ( { 1o } × 1o )
9	2 8	difeq12i	⊢ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) = ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ ( { 1o } × 1o ) )
10		xp01disjl	⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 1o ) ) = ∅
11		disj3	⊢ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 1o ) ) = ∅ ↔ ( { ∅ } × 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) ) )
12	10 11	mpbi	⊢ ( { ∅ } × 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) )
13	1 9 12	3eqtr4i	⊢ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) = ( { ∅ } × 𝐴 )
14		reldom	⊢ Rel ≼
15	14	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
16		1on	⊢ 1o ∈ On
17		djudoml	⊢ ( ( 𝐴 ∈ V ∧ 1o ∈ On ) → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
18	15 16 17	sylancl	⊢ ( ω ≼ 𝐴 → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
19		domtr	⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ≼ ( 𝐴 ⊔ 1o ) ) → ω ≼ ( 𝐴 ⊔ 1o ) )
20	18 19	mpdan	⊢ ( ω ≼ 𝐴 → ω ≼ ( 𝐴 ⊔ 1o ) )
21		infdifsn	⊢ ( ω ≼ ( 𝐴 ⊔ 1o ) → ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) ≈ ( 𝐴 ⊔ 1o ) )
22	20 21	syl	⊢ ( ω ≼ 𝐴 → ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) ≈ ( 𝐴 ⊔ 1o ) )
23	13 22	eqbrtrrid	⊢ ( ω ≼ 𝐴 → ( { ∅ } × 𝐴 ) ≈ ( 𝐴 ⊔ 1o ) )
24	23	ensymd	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ ( { ∅ } × 𝐴 ) )
25		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
26	6 15 25	sylancr	⊢ ( ω ≼ 𝐴 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
27		entr	⊢ ( ( ( 𝐴 ⊔ 1o ) ≈ ( { ∅ } × 𝐴 ) ∧ ( { ∅ } × 𝐴 ) ≈ 𝐴 ) → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )
28	24 26 27	syl2anc	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )