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 ‘ 𝑦 ) )