Metamath Proof Explorer

Theorem dfrecs3

Description: The old definition of transfinite recursion. This version is preferred for development, as it demonstrates the properties of transfinite recursion without relying on well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020)

Ref Expression
Assertion dfrecs3 recs ( 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }

Proof

Step Hyp Ref Expression
1 df-recs ⊢ recs ( 𝐹 ) = wrecs ( E , On , 𝐹 )
2 df-wrecs ⊢ wrecs ( E , On , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) }
3 3anass ⊢ ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ( ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ) )
4 vex ⊢ 𝑥 ∈ V
5 4 elon ⊢ ( 𝑥 ∈ On ↔ Ord 𝑥 )
6 ordsson ⊢ ( Ord 𝑥 → 𝑥 ⊆ On )
7 ordtr ⊢ ( Ord 𝑥 → Tr 𝑥 )
8 6 7 jca ⊢ ( Ord 𝑥 → ( 𝑥 ⊆ On ∧ Tr 𝑥 ) )
9 epweon ⊢ E We On
10 wess ⊢ ( 𝑥 ⊆ On → ( E We On → E We 𝑥 ) )
11 9 10 mpi ⊢ ( 𝑥 ⊆ On → E We 𝑥 )
12 11 anim1ci ⊢ ( ( 𝑥 ⊆ On ∧ Tr 𝑥 ) → ( Tr 𝑥 ∧ E We 𝑥 ) )
13 df-ord ⊢ ( Ord 𝑥 ↔ ( Tr 𝑥 ∧ E We 𝑥 ) )
14 12 13 sylibr ⊢ ( ( 𝑥 ⊆ On ∧ Tr 𝑥 ) → Ord 𝑥 )
15 8 14 impbii ⊢ ( Ord 𝑥 ↔ ( 𝑥 ⊆ On ∧ Tr 𝑥 ) )
16 dftr3 ⊢ ( Tr 𝑥 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥 )
17 ssel2 ⊢ ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
18 predon ⊢ ( 𝑦 ∈ On → Pred ( E , On , 𝑦 ) = 𝑦 )
19 18 sseq1d ⊢ ( 𝑦 ∈ On → ( Pred ( E , On , 𝑦 ) ⊆ 𝑥 ↔ 𝑦 ⊆ 𝑥 ) )
20 17 19 syl ⊢ ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → ( Pred ( E , On , 𝑦 ) ⊆ 𝑥 ↔ 𝑦 ⊆ 𝑥 ) )
21 20 ralbidva ⊢ ( 𝑥 ⊆ On → ( ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ 𝑥 ) )
22 16 21 bitr4id ⊢ ( 𝑥 ⊆ On → ( Tr 𝑥 ↔ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) )
23 22 pm5.32i ⊢ ( ( 𝑥 ⊆ On ∧ Tr 𝑥 ) ↔ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) )
24 5 15 23 3bitri ⊢ ( 𝑥 ∈ On ↔ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) )
25 24 anbi1i ⊢ ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ↔ ( ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) )
26 onelon ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
27 18 reseq2d ⊢ ( 𝑦 ∈ On → ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) = ( 𝑓 ↾ 𝑦 ) )
28 27 fveq2d ⊢ ( 𝑦 ∈ On → ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) )
29 28 eqeq2d ⊢ ( 𝑦 ∈ On → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
30 26 29 syl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
31 30 ralbidva ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
32 31 pm5.32i ⊢ ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
33 25 32 bitr3i ⊢ ( ( ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
34 33 anbi2i ⊢ ( ( 𝑓 Fn 𝑥 ∧ ( ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
35 an12 ⊢ ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
36 3 34 35 3bitri ⊢ ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
37 36 exbii ⊢ ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
38 df-rex ⊢ ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
39 37 38 bitr4i ⊢ ( ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) ↔ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
40 39 abbii ⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
41 40 unieqi ⊢ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ On ∧ ∀ 𝑦 ∈ 𝑥 Pred ( E , On , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( E , On , 𝑦 ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
42 1 2 41 3eqtri ⊢ recs ( 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }