Metamath Proof Explorer

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 ⊢ x | x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y ∈ V

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ z | z ≈ A | ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y = x | x ∈ z | z ≈ A ∧ ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y
2 vex ⊢ x ∈ V
3 breq1 ⊢ z = x → z ≈ A ↔ x ≈ A
4 2 3 elab ⊢ x ∈ z | z ≈ A ↔ x ≈ A
5 breq1 ⊢ z = y → z ≈ A ↔ y ≈ A
6 5 ralab ⊢ ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y ↔ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y
7 4 6 anbi12i ⊢ x ∈ z | z ≈ A ∧ ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y ↔ x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y
8 7 abbii ⊢ x | x ∈ z | z ≈ A ∧ ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y = x | x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y
9 1 8 eqtri ⊢ x ∈ z | z ≈ A | ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y = x | x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y
10 scottex ⊢ x ∈ z | z ≈ A | ∀ y ∈ z | z ≈ A rank ⁡ x ⊆ rank ⁡ y ∈ V
11 9 10 eqeltrri ⊢ x | x ≈ A ∧ ∀ y y ≈ A → rank ⁡ x ⊆ rank ⁡ y ∈ V