Metamath Proof Explorer


Theorem infdiffi

Description: Removing a finite set from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion infdiffi ( ( ω ≼ 𝐴𝐵 ∈ Fin ) → ( 𝐴𝐵 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 difeq2 ( 𝑥 = ∅ → ( 𝐴𝑥 ) = ( 𝐴 ∖ ∅ ) )
2 dif0 ( 𝐴 ∖ ∅ ) = 𝐴
3 1 2 eqtrdi ( 𝑥 = ∅ → ( 𝐴𝑥 ) = 𝐴 )
4 3 breq1d ( 𝑥 = ∅ → ( ( 𝐴𝑥 ) ≈ 𝐴𝐴𝐴 ) )
5 4 imbi2d ( 𝑥 = ∅ → ( ( ω ≼ 𝐴 → ( 𝐴𝑥 ) ≈ 𝐴 ) ↔ ( ω ≼ 𝐴𝐴𝐴 ) ) )
6 difeq2 ( 𝑥 = 𝑦 → ( 𝐴𝑥 ) = ( 𝐴𝑦 ) )
7 6 breq1d ( 𝑥 = 𝑦 → ( ( 𝐴𝑥 ) ≈ 𝐴 ↔ ( 𝐴𝑦 ) ≈ 𝐴 ) )
8 7 imbi2d ( 𝑥 = 𝑦 → ( ( ω ≼ 𝐴 → ( 𝐴𝑥 ) ≈ 𝐴 ) ↔ ( ω ≼ 𝐴 → ( 𝐴𝑦 ) ≈ 𝐴 ) ) )
9 difeq2 ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴𝑥 ) = ( 𝐴 ∖ ( 𝑦 ∪ { 𝑧 } ) ) )
10 difun1 ( 𝐴 ∖ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝐴𝑦 ) ∖ { 𝑧 } )
11 9 10 eqtrdi ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴𝑥 ) = ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) )
12 11 breq1d ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐴𝑥 ) ≈ 𝐴 ↔ ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) )
13 12 imbi2d ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ω ≼ 𝐴 → ( 𝐴𝑥 ) ≈ 𝐴 ) ↔ ( ω ≼ 𝐴 → ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) ) )
14 difeq2 ( 𝑥 = 𝐵 → ( 𝐴𝑥 ) = ( 𝐴𝐵 ) )
15 14 breq1d ( 𝑥 = 𝐵 → ( ( 𝐴𝑥 ) ≈ 𝐴 ↔ ( 𝐴𝐵 ) ≈ 𝐴 ) )
16 15 imbi2d ( 𝑥 = 𝐵 → ( ( ω ≼ 𝐴 → ( 𝐴𝑥 ) ≈ 𝐴 ) ↔ ( ω ≼ 𝐴 → ( 𝐴𝐵 ) ≈ 𝐴 ) ) )
17 reldom Rel ≼
18 17 brrelex2i ( ω ≼ 𝐴𝐴 ∈ V )
19 enrefg ( 𝐴 ∈ V → 𝐴𝐴 )
20 18 19 syl ( ω ≼ 𝐴𝐴𝐴 )
21 domen2 ( ( 𝐴𝑦 ) ≈ 𝐴 → ( ω ≼ ( 𝐴𝑦 ) ↔ ω ≼ 𝐴 ) )
22 21 biimparc ( ( ω ≼ 𝐴 ∧ ( 𝐴𝑦 ) ≈ 𝐴 ) → ω ≼ ( 𝐴𝑦 ) )
23 infdifsn ( ω ≼ ( 𝐴𝑦 ) → ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ ( 𝐴𝑦 ) )
24 22 23 syl ( ( ω ≼ 𝐴 ∧ ( 𝐴𝑦 ) ≈ 𝐴 ) → ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ ( 𝐴𝑦 ) )
25 entr ( ( ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ ( 𝐴𝑦 ) ∧ ( 𝐴𝑦 ) ≈ 𝐴 ) → ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 )
26 24 25 sylancom ( ( ω ≼ 𝐴 ∧ ( 𝐴𝑦 ) ≈ 𝐴 ) → ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 )
27 26 ex ( ω ≼ 𝐴 → ( ( 𝐴𝑦 ) ≈ 𝐴 → ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) )
28 27 a2i ( ( ω ≼ 𝐴 → ( 𝐴𝑦 ) ≈ 𝐴 ) → ( ω ≼ 𝐴 → ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) )
29 28 a1i ( 𝑦 ∈ Fin → ( ( ω ≼ 𝐴 → ( 𝐴𝑦 ) ≈ 𝐴 ) → ( ω ≼ 𝐴 → ( ( 𝐴𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) ) )
30 5 8 13 16 20 29 findcard2 ( 𝐵 ∈ Fin → ( ω ≼ 𝐴 → ( 𝐴𝐵 ) ≈ 𝐴 ) )
31 30 impcom ( ( ω ≼ 𝐴𝐵 ∈ Fin ) → ( 𝐴𝐵 ) ≈ 𝐴 )