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

Metamath Proof Explorer

Theorem pwwf

Description: A power set is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion pwwf ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step Hyp Ref Expression
1 r1rankidb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
2 1 sspwd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
3 rankdmr1 ⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
4 r1sucg ⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
5 3 4 ax-mp ⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) )
6 2 5 sseqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
7 fvex ⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ∈ V
8 7 elpw2 ⊢ ( 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ↔ 𝒫 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
9 6 8 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
10 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
11 10 simpri ⊢ Lim dom 𝑅1
12 limsuc ⊢ ( Lim dom 𝑅1 → ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) )
13 11 12 ax-mp ⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
14 3 13 mpbi ⊢ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1
15 r1sucg ⊢ ( suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
16 14 15 ax-mp ⊢ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) )
17 9 16 eleqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) )
18 r1elwf ⊢ ( 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc suc ( rank ‘ 𝐴 ) ) → 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
19 17 18 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
20 r1elssi ⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
21 pwexr ⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ V )
22 pwidg ⊢ ( 𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴 )
23 21 22 syl ⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ 𝒫 𝐴 )
24 20 23 sseldd ⊢ ( 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
25 19 24 impbii ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝐴 ∈ ∪ ( 𝑅1 “ On ) )