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	⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cardf2	⊢ card : { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑥 ≈ 𝑦 } ⟶ On
2	1	fdmi	⊢ dom card = { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑥 ≈ 𝑦 }
3	2	eleq2i	⊢ ( 𝐴 ∈ dom card ↔ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑥 ≈ 𝑦 } )
4		relen	⊢ Rel ≈
5	4	brrelex2i	⊢ ( 𝑥 ≈ 𝐴 → 𝐴 ∈ V )
6	5	rexlimivw	⊢ ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 → 𝐴 ∈ V )
7		breq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ≈ 𝑦 ↔ 𝑥 ≈ 𝐴 ) )
8	7	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝑦 ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 ) )
9	6 8	elab3	⊢ ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑥 ≈ 𝑦 } ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )
10	3 9	bitri	⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )