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

Metamath Proof Explorer

Theorem tfrlem10

Description: Lemma for transfinite recursion. We define class C by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On . Using this assumption we will prove facts about C that will lead to a contradiction in tfrlem14 , thus showing the domain of recs does in fact equal On . Here we show (under the false assumption) that C is a function extending the domain of recs ( F ) by one. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
tfrlem.3 ⊢ 𝐶 = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
Assertion tfrlem10 ( dom recs ( 𝐹 ) ∈ On → 𝐶 Fn suc dom recs ( 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 tfrlem.3 ⊢ 𝐶 = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
3 fvex ⊢ ( 𝐹 ‘ recs ( 𝐹 ) ) ∈ V
4 funsng ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ ( 𝐹 ‘ recs ( 𝐹 ) ) ∈ V ) → Fun { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
5 3 4 mpan2 ⊢ ( dom recs ( 𝐹 ) ∈ On → Fun { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
6 1 tfrlem7 ⊢ Fun recs ( 𝐹 )
7 5 6 jctil ⊢ ( dom recs ( 𝐹 ) ∈ On → ( Fun recs ( 𝐹 ) ∧ Fun { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
8 3 dmsnop ⊢ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } = { dom recs ( 𝐹 ) }
9 8 ineq2i ⊢ ( dom recs ( 𝐹 ) ∩ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ( dom recs ( 𝐹 ) ∩ { dom recs ( 𝐹 ) } )
10 1 tfrlem8 ⊢ Ord dom recs ( 𝐹 )
11 orddisj ⊢ ( Ord dom recs ( 𝐹 ) → ( dom recs ( 𝐹 ) ∩ { dom recs ( 𝐹 ) } ) = ∅ )
12 10 11 ax-mp ⊢ ( dom recs ( 𝐹 ) ∩ { dom recs ( 𝐹 ) } ) = ∅
13 9 12 eqtri ⊢ ( dom recs ( 𝐹 ) ∩ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ∅
14 funun ⊢ ( ( ( Fun recs ( 𝐹 ) ∧ Fun { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∧ ( dom recs ( 𝐹 ) ∩ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ∅ ) → Fun ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
15 7 13 14 sylancl ⊢ ( dom recs ( 𝐹 ) ∈ On → Fun ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
16 8 uneq2i ⊢ ( dom recs ( 𝐹 ) ∪ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ( dom recs ( 𝐹 ) ∪ { dom recs ( 𝐹 ) } )
17 dmun ⊢ dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ( dom recs ( 𝐹 ) ∪ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
18 df-suc ⊢ suc dom recs ( 𝐹 ) = ( dom recs ( 𝐹 ) ∪ { dom recs ( 𝐹 ) } )
19 16 17 18 3eqtr4i ⊢ dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = suc dom recs ( 𝐹 )
20 df-fn ⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) ↔ ( Fun ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∧ dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = suc dom recs ( 𝐹 ) ) )
21 15 19 20 sylanblrc ⊢ ( dom recs ( 𝐹 ) ∈ On → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) )
22 2 fneq1i ⊢ ( 𝐶 Fn suc dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) )
23 21 22 sylibr ⊢ ( dom recs ( 𝐹 ) ∈ On → 𝐶 Fn suc dom recs ( 𝐹 ) )