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 
|- ( A e. U. ( R1 " On ) <-> U. A e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 r1tr 
 |-  Tr ( R1 ` suc ( rank ` A ) )
2 rankidb 
 |-  ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) )
3 trss 
 |-  ( Tr ( R1 ` suc ( rank ` A ) ) -> ( A e. ( R1 ` suc ( rank ` A ) ) -> A C_ ( R1 ` suc ( rank ` A ) ) ) )
4 1 2 3 mpsyl 
 |-  ( A e. U. ( R1 " On ) -> A C_ ( R1 ` suc ( rank ` A ) ) )
5 rankdmr1 
 |-  ( rank ` A ) e. dom R1
6 r1sucg 
 |-  ( ( rank ` A ) e. dom R1 -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) )
7 5 6 ax-mp 
 |-  ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) )
8 4 7 sseqtrdi 
 |-  ( A e. U. ( R1 " On ) -> A C_ ~P ( R1 ` ( rank ` A ) ) )
9 sspwuni 
 |-  ( A C_ ~P ( R1 ` ( rank ` A ) ) <-> U. A C_ ( R1 ` ( rank ` A ) ) )
10 8 9 sylib 
 |-  ( A e. U. ( R1 " On ) -> U. A C_ ( R1 ` ( rank ` A ) ) )
11 fvex 
 |-  ( R1 ` ( rank ` A ) ) e. _V
12 11 elpw2 
 |-  ( U. A e. ~P ( R1 ` ( rank ` A ) ) <-> U. A C_ ( R1 ` ( rank ` A ) ) )
13 10 12 sylibr 
 |-  ( A e. U. ( R1 " On ) -> U. A e. ~P ( R1 ` ( rank ` A ) ) )
14 13 7 eleqtrrdi 
 |-  ( A e. U. ( R1 " On ) -> U. A e. ( R1 ` suc ( rank ` A ) ) )
15 r1elwf 
 |-  ( U. A e. ( R1 ` suc ( rank ` A ) ) -> U. A e. U. ( R1 " On ) )
16 14 15 syl 
 |-  ( A e. U. ( R1 " On ) -> U. A e. U. ( R1 " On ) )
17 pwwf 
 |-  ( U. A e. U. ( R1 " On ) <-> ~P U. A e. U. ( R1 " On ) )
18 pwuni 
 |-  A C_ ~P U. A
19 sswf 
 |-  ( ( ~P U. A e. U. ( R1 " On ) /\ A C_ ~P U. A ) -> A e. U. ( R1 " On ) )
20 18 19 mpan2 
 |-  ( ~P U. A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) )
21 17 20 sylbi 
 |-  ( U. A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) )
22 16 21 impbii 
 |-  ( A e. U. ( R1 " On ) <-> U. A e. U. ( R1 " On ) )