Metamath Proof Explorer


Theorem rankelg

Description: The membership relation is inherited by the rank function. Closed form of rankel . (Contributed by Scott Fenton, 16-Jul-2015)

Ref Expression
Assertion rankelg ( ( 𝐵𝑉𝐴𝐵 ) → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eleq2 ( 𝑦 = 𝐵 → ( 𝐴𝑦𝐴𝐵 ) )
2 fveq2 ( 𝑦 = 𝐵 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐵 ) )
3 2 eleq2d ( 𝑦 = 𝐵 → ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) )
4 1 3 imbi12d ( 𝑦 = 𝐵 → ( ( 𝐴𝑦 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝑦 ) ) ↔ ( 𝐴𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) ) )
5 vex 𝑦 ∈ V
6 5 rankel ( 𝐴𝑦 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝑦 ) )
7 4 6 vtoclg ( 𝐵𝑉 → ( 𝐴𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) )
8 7 imp ( ( 𝐵𝑉𝐴𝐵 ) → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) )