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 ⊢ A ∈ ⋃ R1 On ↔ ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x

Proof

Step Hyp Ref Expression
1 eluni ⊢ A ∈ ⋃ R1 On ↔ ∃ y A ∈ y ∧ y ∈ R1 On
2 eleq2 ⊢ R1 ⁡ x = y → A ∈ R1 ⁡ x ↔ A ∈ y
3 2 biimprcd ⊢ A ∈ y → R1 ⁡ x = y → A ∈ R1 ⁡ x
4 r1tr ⊢ Tr ⁡ R1 ⁡ x
5 trss ⊢ Tr ⁡ R1 ⁡ x → A ∈ R1 ⁡ x → A ⊆ R1 ⁡ x
6 4 5 ax-mp ⊢ A ∈ R1 ⁡ x → A ⊆ R1 ⁡ x
7 elpwg ⊢ A ∈ R1 ⁡ x → A ∈ 𝒫 R1 ⁡ x ↔ A ⊆ R1 ⁡ x
8 6 7 mpbird ⊢ A ∈ R1 ⁡ x → A ∈ 𝒫 R1 ⁡ x
9 elfvdm ⊢ A ∈ R1 ⁡ x → x ∈ dom ⁡ R1
10 r1sucg ⊢ x ∈ dom ⁡ R1 → R1 ⁡ suc ⁡ x = 𝒫 R1 ⁡ x
11 9 10 syl ⊢ A ∈ R1 ⁡ x → R1 ⁡ suc ⁡ x = 𝒫 R1 ⁡ x
12 8 11 eleqtrrd ⊢ A ∈ R1 ⁡ x → A ∈ R1 ⁡ suc ⁡ x
13 12 a1i ⊢ x ∈ On → A ∈ R1 ⁡ x → A ∈ R1 ⁡ suc ⁡ x
14 3 13 syl9 ⊢ A ∈ y → x ∈ On → R1 ⁡ x = y → A ∈ R1 ⁡ suc ⁡ x
15 14 reximdvai ⊢ A ∈ y → ∃ x ∈ On R1 ⁡ x = y → ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x
16 r1fun ⊢ Fun ⁡ R1
17 fvelima ⊢ Fun ⁡ R1 ∧ y ∈ R1 On → ∃ x ∈ On R1 ⁡ x = y
18 16 17 mpan ⊢ y ∈ R1 On → ∃ x ∈ On R1 ⁡ x = y
19 15 18 impel ⊢ A ∈ y ∧ y ∈ R1 On → ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x
20 19 exlimiv ⊢ ∃ y A ∈ y ∧ y ∈ R1 On → ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x
21 1 20 sylbi ⊢ A ∈ ⋃ R1 On → ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x
22 elfvdm ⊢ A ∈ R1 ⁡ suc ⁡ x → suc ⁡ x ∈ dom ⁡ R1
23 fvelrn ⊢ Fun ⁡ R1 ∧ suc ⁡ x ∈ dom ⁡ R1 → R1 ⁡ suc ⁡ x ∈ ran ⁡ R1
24 16 22 23 sylancr ⊢ A ∈ R1 ⁡ suc ⁡ x → R1 ⁡ suc ⁡ x ∈ ran ⁡ R1
25 rnr1 ⊢ ran ⁡ R1 = R1 On
26 24 25 eleqtrdi ⊢ A ∈ R1 ⁡ suc ⁡ x → R1 ⁡ suc ⁡ x ∈ R1 On
27 elunii ⊢ A ∈ R1 ⁡ suc ⁡ x ∧ R1 ⁡ suc ⁡ x ∈ R1 On → A ∈ ⋃ R1 On
28 26 27 mpdan ⊢ A ∈ R1 ⁡ suc ⁡ x → A ∈ ⋃ R1 On
29 28 rexlimivw ⊢ ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x → A ∈ ⋃ R1 On
30 21 29 impbii ⊢ A ∈ ⋃ R1 On ↔ ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x