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 | z A z y ¬ z x w A w R z w x w y
Assertion wepwso A V R We A T Or 𝒫 A

Proof

Step Hyp Ref Expression
1 wepwso.t T = x y | z A z y ¬ z x w A w R z w x w y
2 2onn 2 𝑜 ω
3 nnord 2 𝑜 ω Ord 2 𝑜
4 2 3 ax-mp Ord 2 𝑜
5 ordwe Ord 2 𝑜 E We 2 𝑜
6 weso E We 2 𝑜 E Or 2 𝑜
7 4 5 6 mp2b E Or 2 𝑜
8 eqid x y | z A x z E y z w A w R z x w = y w = x y | z A x z E y z w A w R z x w = y w
9 8 wemapso R We A E Or 2 𝑜 x y | z A x z E y z w A w R z x w = y w Or 2 𝑜 A
10 7 9 mpan2 R We A x y | z A x z E y z w A w R z x w = y w Or 2 𝑜 A
11 10 adantl A V R We A x y | z A x z E y z w A w R z x w = y w Or 2 𝑜 A
12 elex A V A V
13 eqid a 2 𝑜 A a -1 1 𝑜 = a 2 𝑜 A a -1 1 𝑜
14 1 8 13 wepwsolem A V a 2 𝑜 A a -1 1 𝑜 Isom x y | z A x z E y z w A w R z x w = y w , T 2 𝑜 A 𝒫 A
15 isoso a 2 𝑜 A a -1 1 𝑜 Isom x y | z A x z E y z w A w R z x w = y w , T 2 𝑜 A 𝒫 A x y | z A x z E y z w A w R z x w = y w Or 2 𝑜 A T Or 𝒫 A
16 12 14 15 3syl A V x y | z A x z E y z w A w R z x w = y w Or 2 𝑜 A T Or 𝒫 A
17 16 adantr A V R We A x y | z A x z E y z w A w R z x w = y w Or 2 𝑜 A T Or 𝒫 A
18 11 17 mpbid A V R We A T Or 𝒫 A