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 ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step Hyp Ref Expression
1 r1rankidb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
3 ssun1 ⊢ ( rank ‘ 𝐴 ) ⊆ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
4 rankdmr1 ⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
5 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
6 5 simpri ⊢ Lim dom 𝑅1
7 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
8 6 7 ax-mp ⊢ Ord dom 𝑅1
9 rankdmr1 ⊢ ( rank ‘ 𝐵 ) ∈ dom 𝑅1
10 ordunel ⊢ ( ( Ord dom 𝑅1 ∧ ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ∧ ( rank ‘ 𝐵 ) ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ dom 𝑅1 )
11 8 4 9 10 mp3an ⊢ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ dom 𝑅1
12 r1ord3g ⊢ ( ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ∧ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ⊆ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) )
13 4 11 12 mp2an ⊢ ( ( rank ‘ 𝐴 ) ⊆ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
14 3 13 ax-mp ⊢ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
15 2 14 sstrdi ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → 𝐴 ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
16 r1rankidb ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → 𝐵 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) )
17 16 adantl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → 𝐵 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) )
18 ssun2 ⊢ ( rank ‘ 𝐵 ) ⊆ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
19 r1ord3g ⊢ ( ( ( rank ‘ 𝐵 ) ∈ dom 𝑅1 ∧ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐵 ) ⊆ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) )
20 9 11 19 mp2an ⊢ ( ( rank ‘ 𝐵 ) ⊆ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
21 18 20 ax-mp ⊢ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
22 17 21 sstrdi ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → 𝐵 ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
23 15 22 unssd ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
24 fvex ⊢ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ∈ V
25 24 elpw2 ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ 𝒫 ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
26 23 25 sylibr ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝒫 ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
27 r1sucg ⊢ ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) = 𝒫 ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
28 11 27 ax-mp ⊢ ( 𝑅1 ‘ suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) = 𝒫 ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
29 26 28 eleqtrrdi ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ( 𝑅1 ‘ suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
30 r1elwf ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝑅1 ‘ suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )
31 29 30 syl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )
32 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
33 sswf ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
34 32 33 mpan2 ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
35 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
36 sswf ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ) → 𝐵 ∈ ∪ ( 𝑅1 “ On ) )
37 35 36 mpan2 ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → 𝐵 ∈ ∪ ( 𝑅1 “ On ) )
38 34 37 jca ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) )
39 31 38 impbii ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )