This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tfrlem13

Description: Lemma for transfinite recursion. If recs is a set function, then C is acceptable, and thus a subset of recs , but dom C is bigger than dom recs . This is a contradiction, so recs must be a proper class function. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 14-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 1 tfrlem8 ⊢ Ord dom recs ( 𝐹 )
3 ordirr ⊢ ( Ord dom recs ( 𝐹 ) → ¬ dom recs ( 𝐹 ) ∈ dom recs ( 𝐹 ) )
4 2 3 ax-mp ⊢ ¬ dom recs ( 𝐹 ) ∈ dom recs ( 𝐹 )
5 eqid ⊢ ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
6 1 5 tfrlem12 ⊢ ( recs ( 𝐹 ) ∈ V → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∈ 𝐴 )
7 elssuni ⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∈ 𝐴 → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ ∪ 𝐴 )
8 1 recsfval ⊢ recs ( 𝐹 ) = ∪ 𝐴
9 7 8 sseqtrrdi ⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∈ 𝐴 → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ recs ( 𝐹 ) )
10 dmss ⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ recs ( 𝐹 ) → dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ dom recs ( 𝐹 ) )
11 6 9 10 3syl ⊢ ( recs ( 𝐹 ) ∈ V → dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ dom recs ( 𝐹 ) )
12 2 a1i ⊢ ( recs ( 𝐹 ) ∈ V → Ord dom recs ( 𝐹 ) )
13 dmexg ⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ V )
14 elon2 ⊢ ( dom recs ( 𝐹 ) ∈ On ↔ ( Ord dom recs ( 𝐹 ) ∧ dom recs ( 𝐹 ) ∈ V ) )
15 12 13 14 sylanbrc ⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ On )
16 sucidg ⊢ ( dom recs ( 𝐹 ) ∈ On → dom recs ( 𝐹 ) ∈ suc dom recs ( 𝐹 ) )
17 15 16 syl ⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ suc dom recs ( 𝐹 ) )
18 1 5 tfrlem10 ⊢ ( dom recs ( 𝐹 ) ∈ On → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) )
19 fndm ⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) → dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = suc dom recs ( 𝐹 ) )
20 15 18 19 3syl ⊢ ( recs ( 𝐹 ) ∈ V → dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = suc dom recs ( 𝐹 ) )
21 17 20 eleqtrrd ⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
22 11 21 sseldd ⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ dom recs ( 𝐹 ) )
23 4 22 mto ⊢ ¬ recs ( 𝐹 ) ∈ V