Description: ordelpss with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | ordpss | ⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵 ) ) |
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 𝐵 → ( 𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵 ) ) |