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 abeq2i ( 𝑔𝐵 ↔ ∃ 𝑎 ( 𝑔 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 𝐹 )