Metamath Proof Explorer

Theorem frrlem8

Description: Lemma for well-founded recursion. dom F is closed under predecessor classes. (Contributed by Scott Fenton, 6-Dec-2022)

Ref Expression
Hypotheses frrlem5.1 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
frrlem5.2 ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion frrlem8 ( 𝑧 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )

Proof

Step Hyp Ref Expression
1 frrlem5.1 ⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
2 frrlem5.2 ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
3 vex ⊢ 𝑧 ∈ V
4 3 eldm2 ⊢ ( 𝑧 ∈ dom 𝐹 ↔ ∃ 𝑤 ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐹 )
5 1 2 frrlem5 ⊢ 𝐹 = ∪ 𝐵
6 1 frrlem1 ⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) }
7 6 unieqi ⊢ ∪ 𝐵 = ∪ { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) }
8 5 7 eqtri ⊢ 𝐹 = ∪ { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) }
9 8 eleq2i ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐹 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ∪ { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) } )
10 eluniab ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ∪ { 𝑔 ∣ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) } ↔ ∃ 𝑔 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) )
11 9 10 bitri ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐹 ↔ ∃ 𝑔 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) )
12 simpr2r ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 )
13 vex ⊢ 𝑤 ∈ V
14 3 13 opeldm ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 → 𝑧 ∈ dom 𝑔 )
15 14 adantr ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑧 ∈ dom 𝑔 )
16 simpr1 ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑔 Fn 𝑎 )
17 16 fndmd ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → dom 𝑔 = 𝑎 )
18 15 17 eleqtrd ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑧 ∈ 𝑎 )
19 rsp ⊢ ( ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 → ( 𝑧 ∈ 𝑎 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) )
20 12 18 19 sylc ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 )
21 20 17 sseqtrrd ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝑔 )
22 19.8a ⊢ ( ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) )
23 6 eqabri ⊢ ( 𝑔 ∈ 𝐵 ↔ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) )
24 22 23 sylibr ⊢ ( ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → 𝑔 ∈ 𝐵 )
25 24 adantl ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑔 ∈ 𝐵 )
26 elssuni ⊢ ( 𝑔 ∈ 𝐵 → 𝑔 ⊆ ∪ 𝐵 )
27 25 26 syl ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑔 ⊆ ∪ 𝐵 )
28 27 5 sseqtrrdi ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → 𝑔 ⊆ 𝐹 )
29 dmss ⊢ ( 𝑔 ⊆ 𝐹 → dom 𝑔 ⊆ dom 𝐹 )
30 28 29 syl ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → dom 𝑔 ⊆ dom 𝐹 )
31 21 30 sstrd ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
32 31 expcom ⊢ ( ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) )
33 32 exlimiv ⊢ ( ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ) )
34 33 impcom ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
35 34 exlimiv ⊢ ( ∃ 𝑔 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑔 ∧ ∃ 𝑎 ( 𝑔 Fn 𝑎 ∧ ( 𝑎 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝑎 ) ∧ ∀ 𝑧 ∈ 𝑎 ( 𝑔 ‘ 𝑧 ) = ( 𝑧 𝐺 ( 𝑔 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
36 11 35 sylbi ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
37 36 exlimiv ⊢ ( ∃ 𝑤 ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
38 4 37 sylbi ⊢ ( 𝑧 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )