Metamath Proof Explorer

Theorem tz7.44lem1

Description: The ordered pair abstraction G defined in the hypothesis is a function. This was a lemma for tz7.44-1 , tz7.44-2 , and tz7.44-3 when they used that definition of G . Now, they use the maps-to df-mpt idiom so this lemma is not needed anymore, but is kept in case other applications (for instance in intuitionistic set theory) need it. (Contributed by NM, 23-Apr-1995) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Hypothesis tz7.44lem1.1 ⊢G=xy|x=∅∧y=A∨¬x=∅∨Lim⁡dom⁡x∧y=H⁡x⁡⋃dom⁡x∨Lim⁡dom⁡x∧y=⋃ran⁡x
Assertion tz7.44lem1 ⊢Fun⁡G

Proof

Step Hyp Ref Expression
1 tz7.44lem1.1 ⊢G=xy|x=∅∧y=A∨¬x=∅∨Lim⁡dom⁡x∧y=H⁡x⁡⋃dom⁡x∨Lim⁡dom⁡x∧y=⋃ran⁡x
2 funopab ⊢Fun⁡xy|x=∅∧y=A∨¬x=∅∨Lim⁡dom⁡x∧y=H⁡x⁡⋃dom⁡x∨Lim⁡dom⁡x∧y=⋃ran⁡x↔∀x∃*yx=∅∧y=A∨¬x=∅∨Lim⁡dom⁡x∧y=H⁡x⁡⋃dom⁡x∨Lim⁡dom⁡x∧y=⋃ran⁡x
3 fvex ⊢H⁡x⁡⋃dom⁡x∈V
4 vex ⊢x∈V
5 rnexg ⊢x∈V→ran⁡x∈V
6 uniexg ⊢ran⁡x∈V→⋃ran⁡x∈V
7 4 5 6 mp2b ⊢⋃ran⁡x∈V
8 nlim0 ⊢¬Lim⁡∅
9 dm0 ⊢dom⁡∅=∅
10 limeq ⊢dom⁡∅=∅→Lim⁡dom⁡∅↔Lim⁡∅
11 9 10 ax-mp ⊢Lim⁡dom⁡∅↔Lim⁡∅
12 8 11 mtbir ⊢¬Lim⁡dom⁡∅
13 dmeq ⊢x=∅→dom⁡x=dom⁡∅
14 limeq ⊢dom⁡x=dom⁡∅→Lim⁡dom⁡x↔Lim⁡dom⁡∅
15 13 14 syl ⊢x=∅→Lim⁡dom⁡x↔Lim⁡dom⁡∅
16 15 biimpa ⊢x=∅∧Lim⁡dom⁡x→Lim⁡dom⁡∅
17 12 16 mto ⊢¬x=∅∧Lim⁡dom⁡x
18 3 7 17 moeq3 ⊢∃*yx=∅∧y=A∨¬x=∅∨Lim⁡dom⁡x∧y=H⁡x⁡⋃dom⁡x∨Lim⁡dom⁡x∧y=⋃ran⁡x
19 2 18 mpgbir ⊢Fun⁡xy|x=∅∧y=A∨¬x=∅∨Lim⁡dom⁡x∧y=H⁡x⁡⋃dom⁡x∨Lim⁡dom⁡x∧y=⋃ran⁡x
20 1 funeqi ⊢Fun⁡G↔Fun⁡xy|x=∅∧y=A∨¬x=∅∨Lim⁡dom⁡x∧y=H⁡x⁡⋃dom⁡x∨Lim⁡dom⁡x∧y=⋃ran⁡x
21 19 20 mpbir ⊢Fun⁡G