Metamath Proof Explorer

Theorem tfrlem9a

Description: Lemma for transfinite recursion. Without using ax-rep , show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypothesis tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
Assertion tfrlem9a ( 𝐵 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 1 tfrlem7 ⊢ Fun recs ( 𝐹 )
3 funfvop ⊢ ( ( Fun recs ( 𝐹 ) ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) → ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ recs ( 𝐹 ) )
4 2 3 mpan ⊢ ( 𝐵 ∈ dom recs ( 𝐹 ) → ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ recs ( 𝐹 ) )
5 1 recsfval ⊢ recs ( 𝐹 ) = ∪ 𝐴
6 5 eleq2i ⊢ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ recs ( 𝐹 ) ↔ ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ ∪ 𝐴 )
7 eluni ⊢ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ ∪ 𝐴 ↔ ∃ 𝑔 ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) )
8 6 7 bitri ⊢ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ recs ( 𝐹 ) ↔ ∃ 𝑔 ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) )
9 4 8 sylib ⊢ ( 𝐵 ∈ dom recs ( 𝐹 ) → ∃ 𝑔 ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) )
10 simprr ⊢ ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) → 𝑔 ∈ 𝐴 )
11 vex ⊢ 𝑔 ∈ V
12 1 11 tfrlem3a ⊢ ( 𝑔 ∈ 𝐴 ↔ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) )
13 10 12 sylib ⊢ ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) → ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) )
14 2 a1i ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → Fun recs ( 𝐹 ) )
15 simplrr ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → 𝑔 ∈ 𝐴 )
16 elssuni ⊢ ( 𝑔 ∈ 𝐴 → 𝑔 ⊆ ∪ 𝐴 )
17 15 16 syl ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → 𝑔 ⊆ ∪ 𝐴 )
18 17 5 sseqtrrdi ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → 𝑔 ⊆ recs ( 𝐹 ) )
19 fndm ⊢ ( 𝑔 Fn 𝑧 → dom 𝑔 = 𝑧 )
20 19 ad2antll ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → dom 𝑔 = 𝑧 )
21 simprl ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → 𝑧 ∈ On )
22 20 21 eqeltrd ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → dom 𝑔 ∈ On )
23 eloni ⊢ ( dom 𝑔 ∈ On → Ord dom 𝑔 )
24 22 23 syl ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → Ord dom 𝑔 )
25 simpll ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → 𝐵 ∈ dom recs ( 𝐹 ) )
26 fvexd ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) ∈ V )
27 simplrl ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 )
28 df-br ⊢ ( 𝐵 𝑔 ( recs ( 𝐹 ) ‘ 𝐵 ) ↔ ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 )
29 27 28 sylibr ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → 𝐵 𝑔 ( recs ( 𝐹 ) ‘ 𝐵 ) )
30 breldmg ⊢ ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( recs ( 𝐹 ) ‘ 𝐵 ) ∈ V ∧ 𝐵 𝑔 ( recs ( 𝐹 ) ‘ 𝐵 ) ) → 𝐵 ∈ dom 𝑔 )
31 25 26 29 30 syl3anc ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → 𝐵 ∈ dom 𝑔 )
32 ordelss ⊢ ( ( Ord dom 𝑔 ∧ 𝐵 ∈ dom 𝑔 ) → 𝐵 ⊆ dom 𝑔 )
33 24 31 32 syl2anc ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → 𝐵 ⊆ dom 𝑔 )
34 fun2ssres ⊢ ( ( Fun recs ( 𝐹 ) ∧ 𝑔 ⊆ recs ( 𝐹 ) ∧ 𝐵 ⊆ dom 𝑔 ) → ( recs ( 𝐹 ) ↾ 𝐵 ) = ( 𝑔 ↾ 𝐵 ) )
35 14 18 33 34 syl3anc ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → ( recs ( 𝐹 ) ↾ 𝐵 ) = ( 𝑔 ↾ 𝐵 ) )
36 11 resex ⊢ ( 𝑔 ↾ 𝐵 ) ∈ V
37 36 a1i ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → ( 𝑔 ↾ 𝐵 ) ∈ V )
38 35 37 eqeltrd ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ On ∧ 𝑔 Fn 𝑧 ) ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V )
39 38 expr ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ 𝑧 ∈ On ) → ( 𝑔 Fn 𝑧 → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) )
40 39 adantrd ⊢ ( ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) ∧ 𝑧 ∈ On ) → ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) )
41 40 rexlimdva ⊢ ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) → ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) )
42 13 41 mpd ⊢ ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∧ ( ⟨ 𝐵 , ( recs ( 𝐹 ) ‘ 𝐵 ) ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V )
43 9 42 exlimddv ⊢ ( 𝐵 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V )