Metamath Proof Explorer

Theorem bj-rdg0gALT

Description: Alternate proof of rdg0g . More direct since it bypasses tz7.44-1 and rdg0 (and vtoclg , vtoclga ). (Contributed by NM, 25-Apr-1995) More direct proof. (Revised by BJ, 17-Nov-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-rdg0gALT ⊢A∈V→rec⁡FA⁡∅=A

Proof

Step Hyp Ref Expression
1 rdgdmlim ⊢Lim⁡dom⁡rec⁡FA
2 limomss ⊢Lim⁡dom⁡rec⁡FA→ω⊆dom⁡rec⁡FA
3 1 2 ax-mp ⊢ω⊆dom⁡rec⁡FA
4 peano1 ⊢∅∈ω
5 3 4 sselii ⊢∅∈dom⁡rec⁡FA
6 rdgvalg ⊢∅∈dom⁡rec⁡FA→rec⁡FA⁡∅=x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x⁡rec⁡FA↾∅
7 5 6 ax-mp ⊢rec⁡FA⁡∅=x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x⁡rec⁡FA↾∅
8 res0 ⊢rec⁡FA↾∅=∅
9 8 fveq2i ⊢x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x⁡rec⁡FA↾∅=x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x⁡∅
10 eqid ⊢x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x=x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x
11 simpr ⊢A∈V∧x=∅→x=∅
12 11 iftrued ⊢A∈V∧x=∅→ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x=A
13 0ex ⊢∅∈V
14 13 a1i ⊢A∈V→∅∈V
15 id ⊢A∈V→A∈V
16 10 12 14 15 fvmptd2 ⊢A∈V→x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x⁡∅=A
17 9 16 eqtrid ⊢A∈V→x∈V⟼ifx=∅AifLim⁡dom⁡x⋃ran⁡xF⁡x⁡⋃dom⁡x⁡rec⁡FA↾∅=A
18 7 17 eqtrid ⊢A∈V→rec⁡FA⁡∅=A