# 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 ( 𝐹 )