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 syl5eq ⊢ ( 𝐴 ∈ ω → ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ )
21 disjdif ⊢ ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅
22 20 21 jctil ⊢ ( 𝐴 ∈ ω → ( ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ∧ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) )
23 unen ⊢ ( ( ( { 𝐵 } ≈ { 𝐴 } ∧ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } ) ) ∧ ( ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ∧ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
24 9 22 23 sylancr ⊢ ( 𝐴 ∈ ω → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
25 24 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) )
26 uncom ⊢ ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } )
27 difsnid ⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )
28 26 27 syl5eq ⊢ ( 𝐵 ∈ 𝐴 → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 )
29 28 adantl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 )
30 phplem1 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )
31 25 29 30 3brtr3d ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )