This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { <. x , y >. | ( ( x = (/) /\ y = A ) \/ ( -. ( x = (/) \/ Lim dom x ) /\ y = ( H ` ( x ` U. dom x ) ) ) \/ ( Lim dom x /\ y = U. ran x ) ) }
Assertion tz7.44lem1 
|- Fun G

Proof

Step Hyp Ref Expression
1 tz7.44lem1.1 
 |-  G = { <. x , y >. | ( ( x = (/) /\ y = A ) \/ ( -. ( x = (/) \/ Lim dom x ) /\ y = ( H ` ( x ` U. dom x ) ) ) \/ ( Lim dom x /\ y = U. ran x ) ) }
2 funopab 
 |-  ( Fun { <. x , y >. | ( ( x = (/) /\ y = A ) \/ ( -. ( x = (/) \/ Lim dom x ) /\ y = ( H ` ( x ` U. dom x ) ) ) \/ ( Lim dom x /\ y = U. ran x ) ) } <-> A. x E* y ( ( x = (/) /\ y = A ) \/ ( -. ( x = (/) \/ Lim dom x ) /\ y = ( H ` ( x ` U. dom x ) ) ) \/ ( Lim dom x /\ y = U. ran x ) ) )
3 fvex 
 |-  ( H ` ( x ` U. dom x ) ) e. _V
4 vex 
 |-  x e. _V
5 rnexg 
 |-  ( x e. _V -> ran x e. _V )
6 uniexg 
 |-  ( ran x e. _V -> U. ran x e. _V )
7 4 5 6 mp2b 
 |-  U. ran x e. _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 
 |-  E* y ( ( x = (/) /\ y = A ) \/ ( -. ( x = (/) \/ Lim dom x ) /\ y = ( H ` ( x ` U. dom x ) ) ) \/ ( Lim dom x /\ y = U. ran x ) )
19 2 18 mpgbir 
 |-  Fun { <. x , y >. | ( ( x = (/) /\ y = A ) \/ ( -. ( x = (/) \/ Lim dom x ) /\ y = ( H ` ( x ` U. dom x ) ) ) \/ ( Lim dom x /\ y = U. ran x ) ) }
20 1 funeqi 
 |-  ( Fun G <-> Fun { <. x , y >. | ( ( x = (/) /\ y = A ) \/ ( -. ( x = (/) \/ Lim dom x ) /\ y = ( H ` ( x ` U. dom x ) ) ) \/ ( Lim dom x /\ y = U. ran x ) ) } )
21 19 20 mpbir 
 |-  Fun G