This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fpr2a

Description: Weak version of fpr2 which is useful for proofs that avoid the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024)

Ref Expression
Hypothesis fpr2a.1 ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion fpr2a ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 fpr2a.1 ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
2 fveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
3 id ⊢ ( 𝑦 = 𝑋 → 𝑦 = 𝑋 )
4 predeq3 ⊢ ( 𝑦 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑦 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
5 4 reseq2d ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) = ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
6 3 5 oveq12d ⊢ ( 𝑦 = 𝑋 → ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
7 2 6 eqeq12d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) )
8 7 imbi2d ⊢ ( 𝑦 = 𝑋 → ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) ↔ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) ) )
9 eqid ⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
10 9 1 fprlem1 ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ∧ ℎ ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
11 9 1 10 frrlem10 ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
12 11 expcom ⊢ ( 𝑦 ∈ dom 𝐹 → ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) )
13 8 12 vtoclga ⊢ ( 𝑋 ∈ dom 𝐹 → ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) )
14 13 impcom ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )