Metamath Proof Explorer

Theorem wepwso

Description: A well-ordering induces a strict ordering on the power set.EDITORIAL: when well-orderings are set like, this can be strengthened to remove A e. V . (Contributed by Stefan O'Rear, 18-Jan-2015)

		Ref	Expression
	Hypothesis	wepwso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A ((z \in y \land \neg z \in x) \land \forall w \in A (w R z \to (w \in x \leftrightarrow w \in y)))\}$
	Assertion	wepwso	$⊢ (A \in V \land R We A) \to T Or 𝒫 A$

Proof

Step	Hyp	Ref	Expression
1		wepwso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A ((z \in y \land \neg z \in x) \land \forall w \in A (w R z \to (w \in x \leftrightarrow w \in y)))\}$
2		2onn	$⊢ 2_{𝑜} \in ω$
3		nnord	$⊢ 2_{𝑜} \in ω \to Ord 2_{𝑜}$
4	2 3	ax-mp	$⊢ Ord 2_{𝑜}$
5		ordwe	$⊢ Ord 2_{𝑜} \to E We 2_{𝑜}$
6		weso	$⊢ E We 2_{𝑜} \to E Or 2_{𝑜}$
7	4 5 6	mp2b	$⊢ E Or 2_{𝑜}$
8		eqid	$⊢ \{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\} = \{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
9	8	wemapso	$⊢ (R We A \land E Or 2_{𝑜}) \to \{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\} Or ({2_{𝑜}}^{A})$
10	7 9	mpan2	$⊢ R We A \to \{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\} Or ({2_{𝑜}}^{A})$
11	10	adantl	$⊢ (A \in V \land R We A) \to \{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\} Or ({2_{𝑜}}^{A})$
12		elex	$⊢ A \in V \to A \in V$
13		eqid	$⊢ (a \in ({2_{𝑜}}^{A}) ⟼ a^{-1} [\{1_{𝑜}\}]) = (a \in ({2_{𝑜}}^{A}) ⟼ a^{-1} [\{1_{𝑜}\}])$
14	1 8 13	wepwsolem	$⊢ A \in V \to (a \in ({2_{𝑜}}^{A}) ⟼ a^{-1} [\{1_{𝑜}\}]) {Isom}_{\{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}, T} ({2_{𝑜}}^{A}, 𝒫 A)$
15		isoso	$⊢ (a \in ({2_{𝑜}}^{A}) ⟼ a^{-1} [\{1_{𝑜}\}]) {Isom}_{\{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}, T} ({2_{𝑜}}^{A}, 𝒫 A) \to (\{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\} Or ({2_{𝑜}}^{A}) \leftrightarrow T Or 𝒫 A)$
16	12 14 15	3syl	$⊢ A \in V \to (\{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\} Or ({2_{𝑜}}^{A}) \leftrightarrow T Or 𝒫 A)$
17	16	adantr	$⊢ (A \in V \land R We A) \to (\{⟨x, y⟩ \| \exists z \in A (x (z) E y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\} Or ({2_{𝑜}}^{A}) \leftrightarrow T Or 𝒫 A)$
18	11 17	mpbid	$⊢ (A \in V \land R We A) \to T Or 𝒫 A$