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 ( 𝐴 ∈ 𝑉 → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 rdgdmlim ⊢ Lim dom rec ( 𝐹 , 𝐴 )
2 limomss ⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → ω ⊆ dom rec ( 𝐹 , 𝐴 ) )
3 1 2 ax-mp ⊢ ω ⊆ dom rec ( 𝐹 , 𝐴 )
4 peano1 ⊢ ∅ ∈ ω
5 3 4 sselii ⊢ ∅ ∈ dom rec ( 𝐹 , 𝐴 )
6 rdgvalg ⊢ ( ∅ ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) ) )
7 5 6 ax-mp ⊢ ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) )
8 res0 ⊢ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) = ∅
9 8 fveq2i ⊢ ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) ) = ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ∅ )
10 eqid ⊢ ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) = ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) )
11 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 = ∅ ) → 𝑥 = ∅ )
12 11 iftrued ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 = ∅ ) → if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) = 𝐴 )
13 0ex ⊢ ∅ ∈ V
14 13 a1i ⊢ ( 𝐴 ∈ 𝑉 → ∅ ∈ V )
15 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
16 10 12 14 15 fvmptd2 ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ∅ ) = 𝐴 )
17 9 16 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ ∅ ) ) = 𝐴 )
18 7 17 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ( rec ( 𝐹 , 𝐴 ) ‘ ∅ ) = 𝐴 )