Metamath Proof Explorer

Theorem issmo

Description: Conditions for which A is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011) Avoid ax-13 . (Revised by Gino Giotto, 19-May-2023)

		Ref	Expression
	Hypotheses	issmo.1	$⊢ A : B ⟶ On$
		issmo.2	$⊢ Ord B$
		issmo.3	$⊢ (x \in B \land y \in B) \to (x \in y \to A (x) \in A (y))$
		issmo.4	$⊢ dom A = B$
	Assertion	issmo	$⊢ Smo A$

Proof

Step	Hyp	Ref	Expression
1		issmo.1	$⊢ A : B ⟶ On$
2		issmo.2	$⊢ Ord B$
3		issmo.3	$⊢ (x \in B \land y \in B) \to (x \in y \to A (x) \in A (y))$
4		issmo.4	$⊢ dom A = B$
5	4	feq2i	$⊢ A : dom A ⟶ On \leftrightarrow A : B ⟶ On$
6	1 5	mpbir	$⊢ A : dom A ⟶ On$
7		ordeq	$⊢ dom A = B \to (Ord dom A \leftrightarrow Ord B)$
8	4 7	ax-mp	$⊢ Ord dom A \leftrightarrow Ord B$
9	2 8	mpbir	$⊢ Ord dom A$
10	4	eleq2i	$⊢ x \in dom A \leftrightarrow x \in B$
11	4	eleq2i	$⊢ y \in dom A \leftrightarrow y \in B$
12	10 11 3	syl2anb	$⊢ (x \in dom A \land y \in dom A) \to (x \in y \to A (x) \in A (y))$
13	12	rgen2	$⊢ \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y))$
14		df-smo	$⊢ Smo A \leftrightarrow (A : dom A ⟶ On \land Ord dom A \land \forall x \in dom A \forall y \in dom A (x \in y \to A (x) \in A (y)))$
15	6 9 13 14	mpbir3an	$⊢ Smo A$