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

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 { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( 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