Metamath Proof Explorer

Theorem php2

Description: Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998)

Ref Expression
Assertion php2 ⊢ A ∈ ω ∧ B ⊂ A → B ≺ A

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ x = A → x ∈ ω ↔ A ∈ ω
2 psseq2 ⊢ x = A → B ⊂ x ↔ B ⊂ A
3 1 2 anbi12d ⊢ x = A → x ∈ ω ∧ B ⊂ x ↔ A ∈ ω ∧ B ⊂ A
4 breq2 ⊢ x = A → B ≺ x ↔ B ≺ A
5 3 4 imbi12d ⊢ x = A → x ∈ ω ∧ B ⊂ x → B ≺ x ↔ A ∈ ω ∧ B ⊂ A → B ≺ A
6 vex ⊢ x ∈ V
7 pssss ⊢ B ⊂ x → B ⊆ x
8 ssdomg ⊢ x ∈ V → B ⊆ x → B ≼ x
9 6 7 8 mpsyl ⊢ B ⊂ x → B ≼ x
10 9 adantl ⊢ x ∈ ω ∧ B ⊂ x → B ≼ x
11 php ⊢ x ∈ ω ∧ B ⊂ x → ¬ x ≈ B
12 ensym ⊢ B ≈ x → x ≈ B
13 11 12 nsyl ⊢ x ∈ ω ∧ B ⊂ x → ¬ B ≈ x
14 brsdom ⊢ B ≺ x ↔ B ≼ x ∧ ¬ B ≈ x
15 10 13 14 sylanbrc ⊢ x ∈ ω ∧ B ⊂ x → B ≺ x
16 5 15 vtoclg ⊢ A ∈ ω → A ∈ ω ∧ B ⊂ A → B ≺ A
17 16 anabsi5 ⊢ A ∈ ω ∧ B ⊂ A → B ≺ A