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