This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem php2

Description: Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 20-Nov-2024)

Ref Expression
Assertion php2 ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≺ 𝐴 )

Proof

Step Hyp Ref Expression
1 nnfi ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
2 pssss ⊢ ( 𝐵 ⊊ 𝐴 → 𝐵 ⊆ 𝐴 )
3 ssdomfi ⊢ ( 𝐴 ∈ Fin → ( 𝐵 ⊆ 𝐴 → 𝐵 ≼ 𝐴 ) )
4 3 imp ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ≼ 𝐴 )
5 1 2 4 syl2an ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≼ 𝐴 )
6 php ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝐴 ≈ 𝐵 )
7 ensymfib ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) )
8 7 biimprd ⊢ ( 𝐴 ∈ Fin → ( 𝐵 ≈ 𝐴 → 𝐴 ≈ 𝐵 ) )
9 1 8 syl ⊢ ( 𝐴 ∈ ω → ( 𝐵 ≈ 𝐴 → 𝐴 ≈ 𝐵 ) )
10 9 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ( 𝐵 ≈ 𝐴 → 𝐴 ≈ 𝐵 ) )
11 6 10 mtod ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝐵 ≈ 𝐴 )
12 brsdom ⊢ ( 𝐵 ≺ 𝐴 ↔ ( 𝐵 ≼ 𝐴 ∧ ¬ 𝐵 ≈ 𝐴 ) )
13 5 11 12 sylanbrc ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ≺ 𝐴 )