Metamath Proof Explorer


Theorem phplem2

Description: Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. (Contributed by NM, 11-Jun-1998) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypotheses phplem2.1 𝐴 ∈ V
phplem2.2 𝐵 ∈ V
Assertion phplem2 ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 phplem2.1 𝐴 ∈ V
2 phplem2.2 𝐵 ∈ V
3 snex { ⟨ 𝐵 , 𝐴 ⟩ } ∈ V
4 2 1 f1osn { ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐵 } –1-1-onto→ { 𝐴 }
5 f1oen3g ( ( { ⟨ 𝐵 , 𝐴 ⟩ } ∈ V ∧ { ⟨ 𝐵 , 𝐴 ⟩ } : { 𝐵 } –1-1-onto→ { 𝐴 } ) → { 𝐵 } ≈ { 𝐴 } )
6 3 4 5 mp2an { 𝐵 } ≈ { 𝐴 }
7 1 difexi ( 𝐴 ∖ { 𝐵 } ) ∈ V
8 7 enref ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } )
9 6 8 pm3.2i ( { 𝐵 } ≈ { 𝐴 } ∧ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } ) )
10 incom ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } )
11 difss ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
12 ssrin ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ( 𝐴 ∩ { 𝐴 } ) )
13 11 12 ax-mp ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ( 𝐴 ∩ { 𝐴 } )
14 nnord ( 𝐴 ∈ ω → Ord 𝐴 )
15 orddisj ( Ord 𝐴 → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
16 14 15 syl ( 𝐴 ∈ ω → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
17 13 16 sseqtrid ( 𝐴 ∈ ω → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ∅ )
18 ss0 ( ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ∅ → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) = ∅ )
19 17 18 syl ( 𝐴 ∈ ω → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) = ∅ )
20 10 19 eqtrid ( 𝐴 ∈ ω → ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ )
21 disjdif ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅
22 20 21 jctil ( 𝐴 ∈ ω → ( ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ∧ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) )
23 unen ( ( ( { 𝐵 } ≈ { 𝐴 } ∧ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } ) ) ∧ ( ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ∧ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
24 9 22 23 sylancr ( 𝐴 ∈ ω → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
25 24 adantr ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
26 uncom ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } )
27 difsnid ( 𝐵𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )
28 26 27 eqtrid ( 𝐵𝐴 → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 )
29 28 adantl ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 )
30 phplem1 ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )
31 25 29 30 3brtr3d ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )