Theorem php2

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

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

Proof

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