This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ¬ 𝐴 ∈ V → ∀ 𝑥 ∈ On ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( rank ‘ 𝑦 ) )

Proof

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