Metamath Proof Explorer

Theorem tfrlem7

Description: Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994) (Revised by Mario Carneiro, 24-May-2019)

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

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 1 tfrlem6 ⊢ Rel recs ( 𝐹 )
3 1 recsfval ⊢ recs ( 𝐹 ) = ∪ 𝐴
4 3 eleq2i ⊢ ( ⟨ 𝑥 , 𝑢 ⟩ ∈ recs ( 𝐹 ) ↔ ⟨ 𝑥 , 𝑢 ⟩ ∈ ∪ 𝐴 )
5 eluni ⊢ ( ⟨ 𝑥 , 𝑢 ⟩ ∈ ∪ 𝐴 ↔ ∃ 𝑔 ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) )
6 4 5 bitri ⊢ ( ⟨ 𝑥 , 𝑢 ⟩ ∈ recs ( 𝐹 ) ↔ ∃ 𝑔 ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) )
7 3 eleq2i ⊢ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ recs ( 𝐹 ) ↔ ⟨ 𝑥 , 𝑣 ⟩ ∈ ∪ 𝐴 )
8 eluni ⊢ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ∪ 𝐴 ↔ ∃ ℎ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ∧ ℎ ∈ 𝐴 ) )
9 7 8 bitri ⊢ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ recs ( 𝐹 ) ↔ ∃ ℎ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ∧ ℎ ∈ 𝐴 ) )
10 6 9 anbi12i ⊢ ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ recs ( 𝐹 ) ∧ ⟨ 𝑥 , 𝑣 ⟩ ∈ recs ( 𝐹 ) ) ↔ ( ∃ 𝑔 ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ∧ ∃ ℎ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ∧ ℎ ∈ 𝐴 ) ) )
11 exdistrv ⊢ ( ∃ 𝑔 ∃ ℎ ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ∧ ℎ ∈ 𝐴 ) ) ↔ ( ∃ 𝑔 ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ∧ ∃ ℎ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ∧ ℎ ∈ 𝐴 ) ) )
12 10 11 bitr4i ⊢ ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ recs ( 𝐹 ) ∧ ⟨ 𝑥 , 𝑣 ⟩ ∈ recs ( 𝐹 ) ) ↔ ∃ 𝑔 ∃ ℎ ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ∧ ℎ ∈ 𝐴 ) ) )
13 df-br ⊢ ( 𝑥 𝑔 𝑢 ↔ ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 )
14 df-br ⊢ ( 𝑥 ℎ 𝑣 ↔ ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ )
15 13 14 anbi12i ⊢ ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ↔ ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ) )
16 1 tfrlem5 ⊢ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
17 16 impcom ⊢ ( ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ) → 𝑢 = 𝑣 )
18 15 17 sylanbr ⊢ ( ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ) → 𝑢 = 𝑣 )
19 18 an4s ⊢ ( ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ∧ ℎ ∈ 𝐴 ) ) → 𝑢 = 𝑣 )
20 19 exlimivv ⊢ ( ∃ 𝑔 ∃ ℎ ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ 𝑔 ∧ 𝑔 ∈ 𝐴 ) ∧ ( ⟨ 𝑥 , 𝑣 ⟩ ∈ ℎ ∧ ℎ ∈ 𝐴 ) ) → 𝑢 = 𝑣 )
21 12 20 sylbi ⊢ ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ recs ( 𝐹 ) ∧ ⟨ 𝑥 , 𝑣 ⟩ ∈ recs ( 𝐹 ) ) → 𝑢 = 𝑣 )
22 21 ax-gen ⊢ ∀ 𝑣 ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ recs ( 𝐹 ) ∧ ⟨ 𝑥 , 𝑣 ⟩ ∈ recs ( 𝐹 ) ) → 𝑢 = 𝑣 )
23 22 gen2 ⊢ ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ recs ( 𝐹 ) ∧ ⟨ 𝑥 , 𝑣 ⟩ ∈ recs ( 𝐹 ) ) → 𝑢 = 𝑣 )
24 dffun4 ⊢ ( Fun recs ( 𝐹 ) ↔ ( Rel recs ( 𝐹 ) ∧ ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( ⟨ 𝑥 , 𝑢 ⟩ ∈ recs ( 𝐹 ) ∧ ⟨ 𝑥 , 𝑣 ⟩ ∈ recs ( 𝐹 ) ) → 𝑢 = 𝑣 ) ) )
25 2 23 24 mpbir2an ⊢ Fun recs ( 𝐹 )