Metamath Proof Explorer

Theorem tfrlem15

Description: Lemma for transfinite recursion. Without assuming ax-rep , we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 14-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 1 tfrlem9a ⊢ ( 𝐵 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V )
3 2 adantl ⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V )
4 1 tfrlem13 ⊢ ¬ recs ( 𝐹 ) ∈ V
5 simpr ⊢ ( ( 𝐵 ∈ On ∧ ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) → ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V )
6 resss ⊢ ( recs ( 𝐹 ) ↾ 𝐵 ) ⊆ recs ( 𝐹 )
7 6 a1i ⊢ ( dom recs ( 𝐹 ) ⊆ 𝐵 → ( recs ( 𝐹 ) ↾ 𝐵 ) ⊆ recs ( 𝐹 ) )
8 1 tfrlem6 ⊢ Rel recs ( 𝐹 )
9 resdm ⊢ ( Rel recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 ) )
10 8 9 ax-mp ⊢ ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 )
11 ssres2 ⊢ ( dom recs ( 𝐹 ) ⊆ 𝐵 → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) ⊆ ( recs ( 𝐹 ) ↾ 𝐵 ) )
12 10 11 eqsstrrid ⊢ ( dom recs ( 𝐹 ) ⊆ 𝐵 → recs ( 𝐹 ) ⊆ ( recs ( 𝐹 ) ↾ 𝐵 ) )
13 7 12 eqssd ⊢ ( dom recs ( 𝐹 ) ⊆ 𝐵 → ( recs ( 𝐹 ) ↾ 𝐵 ) = recs ( 𝐹 ) )
14 13 eleq1d ⊢ ( dom recs ( 𝐹 ) ⊆ 𝐵 → ( ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ↔ recs ( 𝐹 ) ∈ V ) )
15 5 14 syl5ibcom ⊢ ( ( 𝐵 ∈ On ∧ ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) → ( dom recs ( 𝐹 ) ⊆ 𝐵 → recs ( 𝐹 ) ∈ V ) )
16 4 15 mtoi ⊢ ( ( 𝐵 ∈ On ∧ ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) → ¬ dom recs ( 𝐹 ) ⊆ 𝐵 )
17 1 tfrlem8 ⊢ Ord dom recs ( 𝐹 )
18 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
19 18 adantr ⊢ ( ( 𝐵 ∈ On ∧ ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) → Ord 𝐵 )
20 ordtri1 ⊢ ( ( Ord dom recs ( 𝐹 ) ∧ Ord 𝐵 ) → ( dom recs ( 𝐹 ) ⊆ 𝐵 ↔ ¬ 𝐵 ∈ dom recs ( 𝐹 ) ) )
21 20 con2bid ⊢ ( ( Ord dom recs ( 𝐹 ) ∧ Ord 𝐵 ) → ( 𝐵 ∈ dom recs ( 𝐹 ) ↔ ¬ dom recs ( 𝐹 ) ⊆ 𝐵 ) )
22 17 19 21 sylancr ⊢ ( ( 𝐵 ∈ On ∧ ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) → ( 𝐵 ∈ dom recs ( 𝐹 ) ↔ ¬ dom recs ( 𝐹 ) ⊆ 𝐵 ) )
23 16 22 mpbird ⊢ ( ( 𝐵 ∈ On ∧ ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) → 𝐵 ∈ dom recs ( 𝐹 ) )
24 3 23 impbida ⊢ ( 𝐵 ∈ On → ( 𝐵 ∈ dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ↾ 𝐵 ) ∈ V ) )