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

Metamath Proof Explorer

Theorem fprresex

Description: The restriction of a function defined by well-founded recursion to the predecessor of an element of its domain is a set. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 fprfung.1 ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
2 1 fprfung ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → Fun 𝐹 )
3 funfvop ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 )
4 2 3 sylan ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 )
5 df-frecs ⊢ frecs ( 𝑅 , 𝐴 , 𝐺 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
6 1 5 eqtri ⊢ 𝐹 = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
7 6 eleq2i ⊢ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ↔ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
8 eluni ⊢ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ↔ ∃ 𝑔 ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) )
9 7 8 bitri ⊢ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ↔ ∃ 𝑔 ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) )
10 4 9 sylib ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ∃ 𝑔 ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) )
11 eqid ⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
12 11 frrlem1 ⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑔 ∣ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) }
13 12 eqabri ⊢ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ↔ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
14 13 biimpi ⊢ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } → ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
15 14 adantl ⊢ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) → ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
16 15 adantl ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
17 3simpa ⊢ ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) )
18 2 ad2antrr ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → Fun 𝐹 )
19 simprlr ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
20 elssuni ⊢ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } → 𝑔 ⊆ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
21 19 20 syl ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑔 ⊆ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
22 21 6 sseqtrrdi ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑔 ⊆ 𝐹 )
23 predeq3 ⊢ ( 𝑤 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑤 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
24 23 sseq1d ⊢ ( 𝑤 = 𝑋 → ( Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ↔ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝑧 ) )
25 simprrr ⊢ ( ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) → ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 )
26 25 adantl ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 )
27 simplr ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑋 ∈ dom 𝐹 )
28 simprll ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 )
29 df-br ⊢ ( 𝑋 𝑔 ( 𝐹 ‘ 𝑋 ) ↔ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 )
30 28 29 sylibr ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑋 𝑔 ( 𝐹 ‘ 𝑋 ) )
31 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
32 breldmg ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑋 ) ∈ V ∧ 𝑋 𝑔 ( 𝐹 ‘ 𝑋 ) ) → 𝑋 ∈ dom 𝑔 )
33 31 32 mp3an2 ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ 𝑋 𝑔 ( 𝐹 ‘ 𝑋 ) ) → 𝑋 ∈ dom 𝑔 )
34 27 30 33 syl2anc ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑋 ∈ dom 𝑔 )
35 simprrl ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑔 Fn 𝑧 )
36 35 fndmd ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → dom 𝑔 = 𝑧 )
37 34 36 eleqtrd ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑋 ∈ 𝑧 )
38 24 26 37 rspcdva ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝑧 )
39 38 36 sseqtrrd ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ dom 𝑔 )
40 fun2ssres ⊢ ( ( Fun 𝐹 ∧ 𝑔 ⊆ 𝐹 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ dom 𝑔 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
41 18 22 39 40 syl3anc ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
42 vex ⊢ 𝑔 ∈ V
43 42 resex ⊢ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V
44 41 43 eqeltrdi ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )
45 44 expr ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V ) )
46 17 45 syl5 ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V ) )
47 46 exlimdv ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝑤 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V ) )
48 16 47 mpd ⊢ ( ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )
49 10 48 exlimddv ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )