Metamath Proof Explorer

Theorem wfrlem17OLD

Description: Obsolete version as of 18-Nov-2024. Without using ax-rep , show that all restrictions of wrecs are sets. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 31-Jul-2020)

Ref Expression
Hypotheses wfrlem17OLD.1 ⊢ 𝑅 We 𝐴
wfrlem17OLD.2 ⊢ 𝑅 Se 𝐴
wfrlem17OLD.3 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion wfrlem17OLD ( 𝑋 ∈ dom 𝐹 → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )

Proof

Step Hyp Ref Expression
1 wfrlem17OLD.1 ⊢ 𝑅 We 𝐴
2 wfrlem17OLD.2 ⊢ 𝑅 Se 𝐴
3 wfrlem17OLD.3 ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
4 1 2 3 wfrfunOLD ⊢ Fun 𝐹
5 funfvop ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 )
6 4 5 mpan ⊢ ( 𝑋 ∈ dom 𝐹 → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 )
7 dfwrecsOLD ⊢ wrecs ( 𝑅 , 𝐴 , 𝐺 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
8 3 7 eqtri ⊢ 𝐹 = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
9 8 eleq2i ⊢ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ↔ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
10 eluni ⊢ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ↔ ∃ 𝑔 ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) )
11 9 10 bitri ⊢ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝐹 ↔ ∃ 𝑔 ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) )
12 6 11 sylib ⊢ ( 𝑋 ∈ dom 𝐹 → ∃ 𝑔 ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) )
13 simprr ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
14 eqid ⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
15 vex ⊢ 𝑔 ∈ V
16 14 15 wfrlem3OLDa ⊢ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ↔ ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
17 13 16 sylib ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) )
18 3simpa ⊢ ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) )
19 simprlr ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
20 elssuni ⊢ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } → 𝑔 ⊆ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } )
21 20 8 sseqtrrdi ⊢ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } → 𝑔 ⊆ 𝐹 )
22 19 21 syl ⊢ ( ( 𝑋 ∈ 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 ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 )
27 simprll ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 )
28 df-br ⊢ ( 𝑋 𝑔 ( 𝐹 ‘ 𝑋 ) ↔ ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 )
29 27 28 sylibr ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑋 𝑔 ( 𝐹 ‘ 𝑋 ) )
30 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
31 breldmg ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑋 ) ∈ V ∧ 𝑋 𝑔 ( 𝐹 ‘ 𝑋 ) ) → 𝑋 ∈ dom 𝑔 )
32 30 31 mp3an2 ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ 𝑋 𝑔 ( 𝐹 ‘ 𝑋 ) ) → 𝑋 ∈ dom 𝑔 )
33 29 32 syldan ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑋 ∈ dom 𝑔 )
34 simprrl ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑔 Fn 𝑧 )
35 34 fndmd ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → dom 𝑔 = 𝑧 )
36 33 35 eleqtrd ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → 𝑋 ∈ 𝑧 )
37 24 26 36 rspcdva ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝑧 )
38 37 35 sseqtrrd ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ dom 𝑔 )
39 fun2ssres ⊢ ( ( Fun 𝐹 ∧ 𝑔 ⊆ 𝐹 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ dom 𝑔 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
40 4 22 38 39 mp3an2i ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) = ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
41 15 resex ⊢ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V
42 40 41 eqeltrdi ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ∧ ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )
43 42 expr ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V ) )
44 18 43 syl5 ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V ) )
45 44 exlimdv ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ∃ 𝑧 ( 𝑔 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐴 ∧ ∀ 𝑤 ∈ 𝑧 Pred ( 𝑅 , 𝐴 , 𝑤 ) ⊆ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑤 ) ) ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V ) )
46 17 45 mpd ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑋 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )
47 12 46 exlimddv ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )