Theorem kardex

Description: The collection of all sets equinumerous to a set A and having the least possible rank is a set. This is the part of the justification of the definition of kard of Enderton p. 222. (Contributed by NM, 14-Dec-2003)

	Ref	Expression
Assertion	kardex	⊢ { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∣ ( 𝑥 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) }
2		vex	⊢ 𝑥 ∈ V
3		breq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ≈ 𝐴 ↔ 𝑥 ≈ 𝐴 ) )
4	2 3	elab	⊢ ( 𝑥 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ↔ 𝑥 ≈ 𝐴 )
5		breq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ≈ 𝐴 ↔ 𝑦 ≈ 𝐴 ) )
6	5	ralab	⊢ ( ∀ 𝑦 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
7	4 6	anbi12i	⊢ ( ( 𝑥 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
8	7	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) } = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
9	1 8	eqtri	⊢ { 𝑥 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
10		scottex	⊢ { 𝑥 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑧 ∣ 𝑧 ≈ 𝐴 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V
11	9 10	eqeltrri	⊢ { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ∈ V