Metamath Proof Explorer


Theorem fun11uni

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004)

Ref Expression
Assertion fun11uni ( ∀ 𝑓𝐴 ( ( Fun 𝑓 ∧ Fun 𝑓 ) ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → ( Fun 𝐴 ∧ Fun 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( Fun 𝑓 ∧ Fun 𝑓 ) → Fun 𝑓 )
2 1 anim1i ( ( ( Fun 𝑓 ∧ Fun 𝑓 ) ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → ( Fun 𝑓 ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) )
3 2 ralimi ( ∀ 𝑓𝐴 ( ( Fun 𝑓 ∧ Fun 𝑓 ) ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → ∀ 𝑓𝐴 ( Fun 𝑓 ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) )
4 fununi ( ∀ 𝑓𝐴 ( Fun 𝑓 ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → Fun 𝐴 )
5 3 4 syl ( ∀ 𝑓𝐴 ( ( Fun 𝑓 ∧ Fun 𝑓 ) ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → Fun 𝐴 )
6 simpr ( ( Fun 𝑓 ∧ Fun 𝑓 ) → Fun 𝑓 )
7 6 anim1i ( ( ( Fun 𝑓 ∧ Fun 𝑓 ) ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → ( Fun 𝑓 ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) )
8 7 ralimi ( ∀ 𝑓𝐴 ( ( Fun 𝑓 ∧ Fun 𝑓 ) ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → ∀ 𝑓𝐴 ( Fun 𝑓 ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) )
9 funcnvuni ( ∀ 𝑓𝐴 ( Fun 𝑓 ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → Fun 𝐴 )
10 8 9 syl ( ∀ 𝑓𝐴 ( ( Fun 𝑓 ∧ Fun 𝑓 ) ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → Fun 𝐴 )
11 5 10 jca ( ∀ 𝑓𝐴 ( ( Fun 𝑓 ∧ Fun 𝑓 ) ∧ ∀ 𝑔𝐴 ( 𝑓𝑔𝑔𝑓 ) ) → ( Fun 𝐴 ∧ Fun 𝐴 ) )