Metamath Proof Explorer

Theorem cardpred

Description: The cardinality function preserves predecessors. (Contributed by BTernaryTau, 18-Jul-2024)

Ref Expression
Assertion cardpred ⊢ A ⊆ dom ⁡ card ∧ B ∈ dom ⁡ card → Pred E card A card ⁡ B = card Pred ≺ A B

Proof

Step Hyp Ref Expression
1 cardf2 ⊢ card : x | ∃ y ∈ On y ≈ x ⟶ On
2 ffun ⊢ card : x | ∃ y ∈ On y ≈ x ⟶ On → Fun ⁡ card
3 2 funfnd ⊢ card : x | ∃ y ∈ On y ≈ x ⟶ On → card Fn dom ⁡ card
4 1 3 mp1i ⊢ A ⊆ dom ⁡ card ∧ B ∈ dom ⁡ card → card Fn dom ⁡ card
5 fvex ⊢ card ⁡ y ∈ V
6 5 epeli ⊢ card ⁡ x E card ⁡ y ↔ card ⁡ x ∈ card ⁡ y
7 cardsdom2 ⊢ x ∈ dom ⁡ card ∧ y ∈ dom ⁡ card → card ⁡ x ∈ card ⁡ y ↔ x ≺ y
8 6 7 bitr2id ⊢ x ∈ dom ⁡ card ∧ y ∈ dom ⁡ card → x ≺ y ↔ card ⁡ x E card ⁡ y
9 8 rgen2 ⊢ ∀ x ∈ dom ⁡ card ∀ y ∈ dom ⁡ card x ≺ y ↔ card ⁡ x E card ⁡ y
10 9 a1i ⊢ A ⊆ dom ⁡ card ∧ B ∈ dom ⁡ card → ∀ x ∈ dom ⁡ card ∀ y ∈ dom ⁡ card x ≺ y ↔ card ⁡ x E card ⁡ y
11 simpl ⊢ A ⊆ dom ⁡ card ∧ B ∈ dom ⁡ card → A ⊆ dom ⁡ card
12 simpr ⊢ A ⊆ dom ⁡ card ∧ B ∈ dom ⁡ card → B ∈ dom ⁡ card
13 4 10 11 12 fnrelpredd ⊢ A ⊆ dom ⁡ card ∧ B ∈ dom ⁡ card → Pred E card A card ⁡ B = card Pred ≺ A B