Metamath Proof Explorer

Theorem unwf

Description: A binary union is well-founded iff its elements are. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion unwf 
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) <-> ( A u. B ) e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 r1rankidb 
 |-  ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) )
2 1 adantr 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> A C_ ( R1 ` ( rank ` A ) ) )
3 ssun1 
 |-  ( rank ` A ) C_ ( ( rank ` A ) u. ( rank ` B ) )
4 rankdmr1 
 |-  ( rank ` A ) e. dom R1
5 r1dmlim 
 |-  Lim dom R1
6 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
7 5 6 ax-mp 
 |-  Ord dom R1
8 rankdmr1 
 |-  ( rank ` B ) e. dom R1
9 ordunel 
 |-  ( ( Ord dom R1 /\ ( rank ` A ) e. dom R1 /\ ( rank ` B ) e. dom R1 ) -> ( ( rank ` A ) u. ( rank ` B ) ) e. dom R1 )
10 7 4 8 9 mp3an 
 |-  ( ( rank ` A ) u. ( rank ` B ) ) e. dom R1
11 r1ord3g 
 |-  ( ( ( rank ` A ) e. dom R1 /\ ( ( rank ` A ) u. ( rank ` B ) ) e. dom R1 ) -> ( ( rank ` A ) C_ ( ( rank ` A ) u. ( rank ` B ) ) -> ( R1 ` ( rank ` A ) ) C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) ) )
12 4 10 11 mp2an 
 |-  ( ( rank ` A ) C_ ( ( rank ` A ) u. ( rank ` B ) ) -> ( R1 ` ( rank ` A ) ) C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) )
13 3 12 ax-mp 
 |-  ( R1 ` ( rank ` A ) ) C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) )
14 2 13 sstrdi 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> A C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) )
15 r1rankidb 
 |-  ( B e. U. ( R1 " On ) -> B C_ ( R1 ` ( rank ` B ) ) )
16 15 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> B C_ ( R1 ` ( rank ` B ) ) )
17 ssun2 
 |-  ( rank ` B ) C_ ( ( rank ` A ) u. ( rank ` B ) )
18 r1ord3g 
 |-  ( ( ( rank ` B ) e. dom R1 /\ ( ( rank ` A ) u. ( rank ` B ) ) e. dom R1 ) -> ( ( rank ` B ) C_ ( ( rank ` A ) u. ( rank ` B ) ) -> ( R1 ` ( rank ` B ) ) C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) ) )
19 8 10 18 mp2an 
 |-  ( ( rank ` B ) C_ ( ( rank ` A ) u. ( rank ` B ) ) -> ( R1 ` ( rank ` B ) ) C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) )
20 17 19 ax-mp 
 |-  ( R1 ` ( rank ` B ) ) C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) )
21 16 20 sstrdi 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> B C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) )
22 14 21 unssd 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( A u. B ) C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) )
23 fvex 
 |-  ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) e. _V
24 23 elpw2 
 |-  ( ( A u. B ) e. ~P ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) <-> ( A u. B ) C_ ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) )
25 22 24 sylibr 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( A u. B ) e. ~P ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) )
26 r1sucg 
 |-  ( ( ( rank ` A ) u. ( rank ` B ) ) e. dom R1 -> ( R1 ` suc ( ( rank ` A ) u. ( rank ` B ) ) ) = ~P ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) ) )
27 10 26 ax-mp 
 |-  ( R1 ` suc ( ( rank ` A ) u. ( rank ` B ) ) ) = ~P ( R1 ` ( ( rank ` A ) u. ( rank ` B ) ) )
28 25 27 eleqtrrdi 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( A u. B ) e. ( R1 ` suc ( ( rank ` A ) u. ( rank ` B ) ) ) )
29 r1elwf 
 |-  ( ( A u. B ) e. ( R1 ` suc ( ( rank ` A ) u. ( rank ` B ) ) ) -> ( A u. B ) e. U. ( R1 " On ) )
30 28 29 syl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( A u. B ) e. U. ( R1 " On ) )
31 ssun1 
 |-  A C_ ( A u. B )
32 sswf 
 |-  ( ( ( A u. B ) e. U. ( R1 " On ) /\ A C_ ( A u. B ) ) -> A e. U. ( R1 " On ) )
33 31 32 mpan2 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> A e. U. ( R1 " On ) )
34 ssun2 
 |-  B C_ ( A u. B )
35 sswf 
 |-  ( ( ( A u. B ) e. U. ( R1 " On ) /\ B C_ ( A u. B ) ) -> B e. U. ( R1 " On ) )
36 34 35 mpan2 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> B e. U. ( R1 " On ) )
37 33 36 jca 
 |-  ( ( A u. B ) e. U. ( R1 " On ) -> ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) )
38 30 37 impbii 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) <-> ( A u. B ) e. U. ( R1 " On ) )