Theorem infpssALT

Description: Alternate proof of infpss , shorter but requiring Replacement ( ax-rep ). (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 16-May-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	infpssALT	⊢ ( ω ≼ 𝐴 → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ominf4	⊢ ¬ ω ∈ FinIV
2		reldom	⊢ Rel ≼
3	2	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
4		isfin4	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ FinIV ↔ ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ) )
5	3 4	syl	⊢ ( ω ≼ 𝐴 → ( 𝐴 ∈ FinIV ↔ ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ) )
6		domfin4	⊢ ( ( 𝐴 ∈ FinIV ∧ ω ≼ 𝐴 ) → ω ∈ FinIV )
7	6	expcom	⊢ ( ω ≼ 𝐴 → ( 𝐴 ∈ FinIV → ω ∈ FinIV ) )
8	5 7	sylbird	⊢ ( ω ≼ 𝐴 → ( ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) → ω ∈ FinIV ) )
9	1 8	mt3i	⊢ ( ω ≼ 𝐴 → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) )