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 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) ) ) }
Assertion wepwso ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → 𝑇 Or 𝒫 𝐴 )

Proof

Step Hyp Ref Expression
1 wepwso.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) ) ) }
2 2onn ⊢ 2o ∈ ω
3 nnord ⊢ ( 2o ∈ ω → Ord 2o )
4 2 3 ax-mp ⊢ Ord 2o
5 ordwe ⊢ ( Ord 2o → E We 2o )
6 weso ⊢ ( E We 2o → E Or 2o )
7 4 5 6 mp2b ⊢ E Or 2o
8 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
9 8 wemapso ⊢ ( ( 𝑅 We 𝐴 ∧ E Or 2o ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } Or ( 2o ↑m 𝐴 ) )
10 7 9 mpan2 ⊢ ( 𝑅 We 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } Or ( 2o ↑m 𝐴 ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } Or ( 2o ↑m 𝐴 ) )
12 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
13 eqid ⊢ ( 𝑎 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑎 “ { 1o } ) ) = ( 𝑎 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑎 “ { 1o } ) )
14 1 8 13 wepwsolem ⊢ ( 𝐴 ∈ V → ( 𝑎 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑎 “ { 1o } ) ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } , 𝑇 ( ( 2o ↑m 𝐴 ) , 𝒫 𝐴 ) )
15 isoso ⊢ ( ( 𝑎 ∈ ( 2o ↑m 𝐴 ) ↦ ( ◡ 𝑎 “ { 1o } ) ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } , 𝑇 ( ( 2o ↑m 𝐴 ) , 𝒫 𝐴 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } Or ( 2o ↑m 𝐴 ) ↔ 𝑇 Or 𝒫 𝐴 ) )
16 12 14 15 3syl ⊢ ( 𝐴 ∈ 𝑉 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } Or ( 2o ↑m 𝐴 ) ↔ 𝑇 Or 𝒫 𝐴 ) )
17 16 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) E ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } Or ( 2o ↑m 𝐴 ) ↔ 𝑇 Or 𝒫 𝐴 ) )
18 11 17 mpbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → 𝑇 Or 𝒫 𝐴 )