Metamath Proof Explorer

Theorem iscard2

Description: Two ways to express the property of being a cardinal number. Definition 8 of Suppes p. 225. (Contributed by Mario Carneiro, 15-Jan-2013)

Ref Expression
Assertion iscard2 ⊢ card ⁡ A = A ↔ A ∈ On ∧ ∀ x ∈ On A ≈ x → A ⊆ x

Proof

Step Hyp Ref Expression
1 cardon ⊢ card ⁡ A ∈ On
2 eleq1 ⊢ card ⁡ A = A → card ⁡ A ∈ On ↔ A ∈ On
3 1 2 mpbii ⊢ card ⁡ A = A → A ∈ On
4 cardonle ⊢ A ∈ On → card ⁡ A ⊆ A
5 4 biantrurd ⊢ A ∈ On → A ⊆ card ⁡ A ↔ card ⁡ A ⊆ A ∧ A ⊆ card ⁡ A
6 eqss ⊢ card ⁡ A = A ↔ card ⁡ A ⊆ A ∧ A ⊆ card ⁡ A
7 5 6 syl6rbbr ⊢ A ∈ On → card ⁡ A = A ↔ A ⊆ card ⁡ A
8 oncardval ⊢ A ∈ On → card ⁡ A = ⋂ y ∈ On | y ≈ A
9 8 sseq2d ⊢ A ∈ On → A ⊆ card ⁡ A ↔ A ⊆ ⋂ y ∈ On | y ≈ A
10 7 9 bitrd ⊢ A ∈ On → card ⁡ A = A ↔ A ⊆ ⋂ y ∈ On | y ≈ A
11 ssint ⊢ A ⊆ ⋂ y ∈ On | y ≈ A ↔ ∀ x ∈ y ∈ On | y ≈ A A ⊆ x
12 breq1 ⊢ y = x → y ≈ A ↔ x ≈ A
13 12 elrab ⊢ x ∈ y ∈ On | y ≈ A ↔ x ∈ On ∧ x ≈ A
14 ensymb ⊢ x ≈ A ↔ A ≈ x
15 14 anbi2i ⊢ x ∈ On ∧ x ≈ A ↔ x ∈ On ∧ A ≈ x
16 13 15 bitri ⊢ x ∈ y ∈ On | y ≈ A ↔ x ∈ On ∧ A ≈ x
17 16 imbi1i ⊢ x ∈ y ∈ On | y ≈ A → A ⊆ x ↔ x ∈ On ∧ A ≈ x → A ⊆ x
18 impexp ⊢ x ∈ On ∧ A ≈ x → A ⊆ x ↔ x ∈ On → A ≈ x → A ⊆ x
19 17 18 bitri ⊢ x ∈ y ∈ On | y ≈ A → A ⊆ x ↔ x ∈ On → A ≈ x → A ⊆ x
20 19 ralbii2 ⊢ ∀ x ∈ y ∈ On | y ≈ A A ⊆ x ↔ ∀ x ∈ On A ≈ x → A ⊆ x
21 11 20 bitri ⊢ A ⊆ ⋂ y ∈ On | y ≈ A ↔ ∀ x ∈ On A ≈ x → A ⊆ x
22 10 21 syl6bb ⊢ A ∈ On → card ⁡ A = A ↔ ∀ x ∈ On A ≈ x → A ⊆ x
23 3 22 biadanii ⊢ card ⁡ A = A ↔ A ∈ On ∧ ∀ x ∈ On A ≈ x → A ⊆ x