Theorem ordpss

Description: ordelpss with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	ordpss	⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ordelord	⊢ ( ( Ord 𝐵 ∧ 𝐴 ∈ 𝐵 ) → Ord 𝐴 )
2	1	ex	⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → Ord 𝐴 ) )
3	2	ancrd	⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → ( Ord 𝐴 ∧ 𝐴 ∈ 𝐵 ) ) )
4		ordelpss	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )
5	4	ancoms	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )
6	5	biimpd	⊢ ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵 ) )
7	6	expimpd	⊢ ( Ord 𝐵 → ( ( Ord 𝐴 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ⊊ 𝐵 ) )
8	3 7	syld	⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵 ) )