Metamath Proof Explorer

Theorem rankr1a

Description: A relationship between rank and R1 , clearly equivalent to ssrankr1 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b for the subset version. (Contributed by Raph Levien, 29-May-2004)

Ref Expression
Hypothesis rankid.1 ⊢ A ∈ V
Assertion rankr1a ⊢ B ∈ On → A ∈ R1 ⁡ B ↔ rank ⁡ A ∈ B

Proof

Step Hyp Ref Expression
1 rankid.1 ⊢ A ∈ V
2 1 ssrankr1 ⊢ B ∈ On → B ⊆ rank ⁡ A ↔ ¬ A ∈ R1 ⁡ B
3 rankon ⊢ rank ⁡ A ∈ On
4 ontri1 ⊢ B ∈ On ∧ rank ⁡ A ∈ On → B ⊆ rank ⁡ A ↔ ¬ rank ⁡ A ∈ B
5 3 4 mpan2 ⊢ B ∈ On → B ⊆ rank ⁡ A ↔ ¬ rank ⁡ A ∈ B
6 2 5 bitr3d ⊢ B ∈ On → ¬ A ∈ R1 ⁡ B ↔ ¬ rank ⁡ A ∈ B
7 6 con4bid ⊢ B ∈ On → A ∈ R1 ⁡ B ↔ rank ⁡ A ∈ B