inawinalem

		Ref	Expression
	Assertion	inawinalem	$⊢ A \in On \to (\forall x \in A 𝒫 x ≺ A \to \forall x \in A \exists y \in A x ≺ y)$

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ 𝒫 x ≺ A \to 𝒫 x ≼ A$
2		ondomen	$⊢ (A \in On \land 𝒫 x ≼ A) \to 𝒫 x \in dom card$
3		isnum2	$⊢ 𝒫 x \in dom card \leftrightarrow \exists y \in On y \approx 𝒫 x$
4	2 3	sylib	$⊢ (A \in On \land 𝒫 x ≼ A) \to \exists y \in On y \approx 𝒫 x$
5	1 4	sylan2	$⊢ (A \in On \land 𝒫 x ≺ A) \to \exists y \in On y \approx 𝒫 x$
6		ensdomtr	$⊢ (y \approx 𝒫 x \land 𝒫 x ≺ A) \to y ≺ A$
7	6	ad2ant2l	$⊢ ((y \in On \land y \approx 𝒫 x) \land (A \in On \land 𝒫 x ≺ A)) \to y ≺ A$
8		sdomel	$⊢ (y \in On \land A \in On) \to (y ≺ A \to y \in A)$
9	8	ad2ant2r	$⊢ ((y \in On \land y \approx 𝒫 x) \land (A \in On \land 𝒫 x ≺ A)) \to (y ≺ A \to y \in A)$
10	7 9	mpd	$⊢ ((y \in On \land y \approx 𝒫 x) \land (A \in On \land 𝒫 x ≺ A)) \to y \in A$
11		vex	$⊢ x \in V$
12	11	canth2	$⊢ x ≺ 𝒫 x$
13		ensym	$⊢ y \approx 𝒫 x \to 𝒫 x \approx y$
14		sdomentr	$⊢ (x ≺ 𝒫 x \land 𝒫 x \approx y) \to x ≺ y$
15	12 13 14	sylancr	$⊢ y \approx 𝒫 x \to x ≺ y$
16	15	ad2antlr	$⊢ ((y \in On \land y \approx 𝒫 x) \land (A \in On \land 𝒫 x ≺ A)) \to x ≺ y$
17	10 16	jca	$⊢ ((y \in On \land y \approx 𝒫 x) \land (A \in On \land 𝒫 x ≺ A)) \to (y \in A \land x ≺ y)$
18	17	expcom	$⊢ (A \in On \land 𝒫 x ≺ A) \to ((y \in On \land y \approx 𝒫 x) \to (y \in A \land x ≺ y))$
19	18	reximdv2	$⊢ (A \in On \land 𝒫 x ≺ A) \to (\exists y \in On y \approx 𝒫 x \to \exists y \in A x ≺ y)$
20	5 19	mpd	$⊢ (A \in On \land 𝒫 x ≺ A) \to \exists y \in A x ≺ y$
21	20	ex	$⊢ A \in On \to (𝒫 x ≺ A \to \exists y \in A x ≺ y)$
22	21	ralimdv	$⊢ A \in On \to (\forall x \in A 𝒫 x ≺ A \to \forall x \in A \exists y \in A x ≺ y)$

Metamath Proof Explorer

Theorem inawinalem

Proof