Metamath Proof Explorer

Theorem unbndrank

Description: The elements of a proper class have unbounded rank. Exercise 2 of TakeutiZaring p. 80. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion unbndrank ⊢ ¬ A ∈ V → ∀ x ∈ On ∃ y ∈ A x ∈ rank ⁡ y

Proof

Step Hyp Ref Expression
1 rankon ⊢ rank ⁡ y ∈ On
2 ontri1 ⊢ rank ⁡ y ∈ On ∧ x ∈ On → rank ⁡ y ⊆ x ↔ ¬ x ∈ rank ⁡ y
3 1 2 mpan ⊢ x ∈ On → rank ⁡ y ⊆ x ↔ ¬ x ∈ rank ⁡ y
4 3 ralbidv ⊢ x ∈ On → ∀ y ∈ A rank ⁡ y ⊆ x ↔ ∀ y ∈ A ¬ x ∈ rank ⁡ y
5 ralnex ⊢ ∀ y ∈ A ¬ x ∈ rank ⁡ y ↔ ¬ ∃ y ∈ A x ∈ rank ⁡ y
6 4 5 bitrdi ⊢ x ∈ On → ∀ y ∈ A rank ⁡ y ⊆ x ↔ ¬ ∃ y ∈ A x ∈ rank ⁡ y
7 6 rexbiia ⊢ ∃ x ∈ On ∀ y ∈ A rank ⁡ y ⊆ x ↔ ∃ x ∈ On ¬ ∃ y ∈ A x ∈ rank ⁡ y
8 rexnal ⊢ ∃ x ∈ On ¬ ∃ y ∈ A x ∈ rank ⁡ y ↔ ¬ ∀ x ∈ On ∃ y ∈ A x ∈ rank ⁡ y
9 7 8 bitri ⊢ ∃ x ∈ On ∀ y ∈ A rank ⁡ y ⊆ x ↔ ¬ ∀ x ∈ On ∃ y ∈ A x ∈ rank ⁡ y
10 bndrank ⊢ ∃ x ∈ On ∀ y ∈ A rank ⁡ y ⊆ x → A ∈ V
11 9 10 sylbir ⊢ ¬ ∀ x ∈ On ∃ y ∈ A x ∈ rank ⁡ y → A ∈ V
12 11 con1i ⊢ ¬ A ∈ V → ∀ x ∈ On ∃ y ∈ A x ∈ rank ⁡ y