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 𝒫 𝐴 )