This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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