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