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

Metamath Proof Explorer

Theorem uniwf

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

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

Proof

Step Hyp Ref Expression
1 r1tr ⊢ Tr ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) )
2 rankidb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
3 trss ⊢ ( Tr ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ) )
4 1 2 3 mpsyl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
5 rankdmr1 ⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
6 r1sucg ⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
7 5 6 ax-mp ⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) )
8 4 7 sseqtrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
9 sspwuni ⊢ ( 𝐴 ⊆ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ↔ ∪ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
10 8 9 sylib ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
11 fvex ⊢ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∈ V
12 11 elpw2 ⊢ ( ∪ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ↔ ∪ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
13 10 12 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
14 13 7 eleqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
15 r1elwf ⊢ ( ∪ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
16 14 15 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
17 pwwf ⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
18 pwuni ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
19 sswf ⊢ ( ( 𝒫 ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
20 18 19 mpan2 ⊢ ( 𝒫 ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
21 17 20 sylbi ⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
22 16 21 impbii ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )