![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rankr1a | Structured version Visualization version GIF version |
Description: A relationship between rank and 𝑅1, clearly equivalent to ssrankr1 8869 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b 8898 for the subset version. (Contributed by Raph Levien, 29-May-2004.) |
Ref | Expression |
---|---|
rankid.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
rankr1a | ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rankid.1 | . . . 4 ⊢ 𝐴 ∈ V | |
2 | 1 | ssrankr1 8869 | . . 3 ⊢ (𝐵 ∈ On → (𝐵 ⊆ (rank‘𝐴) ↔ ¬ 𝐴 ∈ (𝑅1‘𝐵))) |
3 | rankon 8829 | . . . 4 ⊢ (rank‘𝐴) ∈ On | |
4 | ontri1 5916 | . . . 4 ⊢ ((𝐵 ∈ On ∧ (rank‘𝐴) ∈ On) → (𝐵 ⊆ (rank‘𝐴) ↔ ¬ (rank‘𝐴) ∈ 𝐵)) | |
5 | 3, 4 | mpan2 709 | . . 3 ⊢ (𝐵 ∈ On → (𝐵 ⊆ (rank‘𝐴) ↔ ¬ (rank‘𝐴) ∈ 𝐵)) |
6 | 2, 5 | bitr3d 270 | . 2 ⊢ (𝐵 ∈ On → (¬ 𝐴 ∈ (𝑅1‘𝐵) ↔ ¬ (rank‘𝐴) ∈ 𝐵)) |
7 | 6 | con4bid 306 | 1 ⊢ (𝐵 ∈ On → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∈ wcel 2137 Vcvv 3338 ⊆ wss 3713 Oncon0 5882 ‘cfv 6047 𝑅1cr1 8796 rankcrnk 8797 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-8 2139 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-rep 4921 ax-sep 4931 ax-nul 4939 ax-pow 4990 ax-pr 5053 ax-un 7112 ax-reg 8660 ax-inf2 8709 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-ral 3053 df-rex 3054 df-reu 3055 df-rab 3057 df-v 3340 df-sbc 3575 df-csb 3673 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-pss 3729 df-nul 4057 df-if 4229 df-pw 4302 df-sn 4320 df-pr 4322 df-tp 4324 df-op 4326 df-uni 4587 df-int 4626 df-iun 4672 df-br 4803 df-opab 4863 df-mpt 4880 df-tr 4903 df-id 5172 df-eprel 5177 df-po 5185 df-so 5186 df-fr 5223 df-we 5225 df-xp 5270 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-rn 5275 df-res 5276 df-ima 5277 df-pred 5839 df-ord 5885 df-on 5886 df-lim 5887 df-suc 5888 df-iota 6010 df-fun 6049 df-fn 6050 df-f 6051 df-f1 6052 df-fo 6053 df-f1o 6054 df-fv 6055 df-om 7229 df-wrecs 7574 df-recs 7635 df-rdg 7673 df-r1 8798 df-rank 8799 |
This theorem is referenced by: r1val2 8871 r1pwALT 8880 elhf2 32586 |
Copyright terms: Public domain | W3C validator |