Metamath Proof Explorer

Theorem rankwflemb

Description: Two ways of expressing that a set is well-founded. (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014) (Proof shortened by BJ, 29-Sep-2026)

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 r1fun ⊢ Fun 𝑅1
17 fvelima ⊢ ( ( Fun 𝑅1 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
18 16 17 mpan ⊢ ( 𝑦 ∈ ( 𝑅1 “ On ) → ∃ 𝑥 ∈ On ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
19 15 18 impel ⊢ ( ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
20 19 exlimiv ⊢ ( ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ( 𝑅1 “ On ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
21 1 20 sylbi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
22 elfvdm ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → suc 𝑥 ∈ dom 𝑅1 )
23 fvelrn ⊢ ( ( Fun 𝑅1 ∧ suc 𝑥 ∈ dom 𝑅1 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ran 𝑅1 )
24 16 22 23 sylancr ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ran 𝑅1 )
25 rnr1 ⊢ ran 𝑅1 = ( 𝑅1 “ On )
26 24 25 eleqtrdi ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑅1 ‘ suc 𝑥 ) ∈ ( 𝑅1 “ On ) )
27 elunii ⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ∧ ( 𝑅1 ‘ suc 𝑥 ) ∈ ( 𝑅1 “ On ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
28 26 27 mpdan ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
29 28 rexlimivw ⊢ ( ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
30 21 29 impbii ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )