This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rankwflemb

Description: Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion rankwflemb ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )

Proof

Step Hyp Ref Expression
1 eluni ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) )
2 eleq2 ⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ∈ 𝑦 ) )
3 2 biimprcd ⊢ ( 𝐴 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
4 r1tr ⊢ Tr ( 𝑅1 ‘ 𝑥 )
5 trss ⊢ ( Tr ( 𝑅1 ‘ 𝑥 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
6 4 5 ax-mp ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) )
7 elpwg ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
8 6 7 mpbird ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) )
9 elfvdm ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝑥 ∈ dom 𝑅1 )
10 r1sucg ⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
11 9 10 syl ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
12 8 11 eleqtrrd ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
13 12 a1i ⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
14 3 13 syl9 ⊢ ( 𝐴 ∈ 𝑦 → ( 𝑥 ∈ On → ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) ) )
15 14 reximdvai ⊢ ( 𝐴 ∈ 𝑦 → ( ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
16 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
17 16 simpli ⊢ Fun 𝑅1
18 fvelima ⊢ ( ( Fun 𝑅1 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
19 17 18 mpan ⊢ ( 𝑦 ∈ ( 𝑅1 “ On ) → ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
20 15 19 impel ⊢ ( ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
21 20 exlimiv ⊢ ( ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
22 1 21 sylbi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
23 elfvdm ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → suc 𝑥 ∈ dom 𝑅1 )
24 fvelrn ⊢ ( ( Fun 𝑅1 ∧ suc 𝑥 ∈ dom 𝑅1 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ran 𝑅1 )
25 17 23 24 sylancr ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ran 𝑅1 )
26 df-ima ⊢ ( 𝑅1 “ On ) = ran ( 𝑅1 ↾ On )
27 funrel ⊢ ( Fun 𝑅1 → Rel 𝑅1 )
28 17 27 ax-mp ⊢ Rel 𝑅1
29 16 simpri ⊢ Lim dom 𝑅1
30 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
31 ordsson ⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
32 29 30 31 mp2b ⊢ dom 𝑅1 ⊆ On
33 relssres ⊢ ( ( Rel 𝑅1 ∧ dom 𝑅1 ⊆ On ) → ( 𝑅1 ↾ On ) = 𝑅1 )
34 28 32 33 mp2an ⊢ ( 𝑅1 ↾ On ) = 𝑅1
35 34 rneqi ⊢ ran ( 𝑅1 ↾ On ) = ran 𝑅1
36 26 35 eqtri ⊢ ( 𝑅1 “ On ) = ran 𝑅1
37 25 36 eleqtrrdi ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ( 𝑅1 “ On ) )
38 elunii ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ∧ ( 𝑅1 ‘ suc 𝑥 ) ∈ ( 𝑅1 “ On ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
39 37 38 mpdan ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
40 39 rexlimivw ⊢ ( ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
41 22 40 impbii ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )