Metamath Proof Explorer

Theorem isnum2

Description: A way to express well-orderability without bound or distinct variables. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion isnum2 ⊢ A ∈ dom ⁡ card ↔ ∃ x ∈ On x ≈ A

Proof

Step Hyp Ref Expression
1 cardf2 ⊢ card : y | ∃ x ∈ On x ≈ y ⟶ On
2 1 fdmi ⊢ dom ⁡ card = y | ∃ x ∈ On x ≈ y
3 2 eleq2i ⊢ A ∈ dom ⁡ card ↔ A ∈ y | ∃ x ∈ On x ≈ y
4 relen ⊢ Rel ⁡ ≈
5 4 brrelex2i ⊢ x ≈ A → A ∈ V
6 5 rexlimivw ⊢ ∃ x ∈ On x ≈ A → A ∈ V
7 breq2 ⊢ y = A → x ≈ y ↔ x ≈ A
8 7 rexbidv ⊢ y = A → ∃ x ∈ On x ≈ y ↔ ∃ x ∈ On x ≈ A
9 6 8 elab3 ⊢ A ∈ y | ∃ x ∈ On x ≈ y ↔ ∃ x ∈ On x ≈ A
10 3 9 bitri ⊢ A ∈ dom ⁡ card ↔ ∃ x ∈ On x ≈ A