This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Infinity Rank 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 ⊢ 𝐴 ∈ V
Assertion
rankr1a ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
rankid.1 ⊢ 𝐴 ∈ V
2
1
ssrankr1 ⊢ ( 𝐵 ∈ On → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) )
3
rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
4
ontri1 ⊢ ( ( 𝐵 ∈ On ∧ ( rank ‘ 𝐴 ) ∈ On ) → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
5
3 4
mpan2 ⊢ ( 𝐵 ∈ On → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
6
2 5
bitr3d ⊢ ( 𝐵 ∈ On → ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
7
6
con4bid ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )