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 ⁡ F A ⁡ ∅ = A

Proof

Step Hyp Ref Expression
1 rdgdmlim ⊢ Lim ⁡ dom ⁡ rec ⁡ F A
2 limomss ⊢ Lim ⁡ dom ⁡ rec ⁡ F A → ω ⊆ dom ⁡ rec ⁡ F A
3 1 2 ax-mp ⊢ ω ⊆ dom ⁡ rec ⁡ F A
4 peano1 ⊢ ∅ ∈ ω
5 3 4 sselii ⊢ ∅ ∈ dom ⁡ rec ⁡ F A
6 rdgvalg ⊢ ∅ ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ ∅ = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x ⁡ rec ⁡ F A ↾ ∅
7 5 6 ax-mp ⊢ rec ⁡ F A ⁡ ∅ = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x ⁡ rec ⁡ F A ↾ ∅
8 res0 ⊢ rec ⁡ F A ↾ ∅ = ∅
9 8 fveq2i ⊢ x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x ⁡ rec ⁡ F A ↾ ∅ = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x ⁡ ∅
10 eqid ⊢ x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x = x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x
11 simpr ⊢ A ∈ V ∧ x = ∅ → x = ∅
12 11 iftrued ⊢ A ∈ V ∧ x = ∅ → if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ 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 ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x ⁡ ∅ = A
17 9 16 eqtrid ⊢ A ∈ V → x ∈ V ⟼ if x = ∅ A if Lim ⁡ dom ⁡ x ⋃ ran ⁡ x F ⁡ x ⁡ ⋃ dom ⁡ x ⁡ rec ⁡ F A ↾ ∅ = A
18 7 17 eqtrid ⊢ A ∈ V → rec ⁡ F A ⁡ ∅ = A