cardpred

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

		Ref	Expression
	Assertion	cardpred	$⊢ (A \subseteq dom card \land B \in dom card) \to Pred (E, card [A], card (B)) = card [Pred (≺ A B)]$

Step	Hyp	Ref	Expression
1		cardf2	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On$
2		ffun	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On \to Fun card$
3	2	funfnd	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On \to card Fn dom card$
4	1 3	mp1i	$⊢ (A \subseteq dom card \land B \in dom card) \to card Fn dom card$
5		fvex	$⊢ card (y) \in V$
6	5	epeli	$⊢ card (x) E card (y) \leftrightarrow card (x) \in card (y)$
7		cardsdom2	$⊢ (x \in dom card \land y \in dom card) \to (card (x) \in card (y) \leftrightarrow x ≺ y)$
8	6 7	bitr2id	$⊢ (x \in dom card \land y \in dom card) \to (x ≺ y \leftrightarrow card (x) E card (y))$
9	8	rgen2	$⊢ \forall x \in dom card \forall y \in dom card (x ≺ y \leftrightarrow card (x) E card (y))$
10	9	a1i	$⊢ (A \subseteq dom card \land B \in dom card) \to \forall x \in dom card \forall y \in dom card (x ≺ y \leftrightarrow card (x) E card (y))$
11		simpl	$⊢ (A \subseteq dom card \land B \in dom card) \to A \subseteq dom card$
12		simpr	$⊢ (A \subseteq dom card \land B \in dom card) \to B \in dom card$
13	4 10 11 12	fnrelpredd	$⊢ (A \subseteq dom card \land B \in dom card) \to Pred (E, card [A], card (B)) = card [Pred (≺ A B)]$

Metamath Proof Explorer