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 ⁡ ⋃ dom ⁡ x ∨ Lim ⁡ dom ⁡ x ∧ y = ⋃ 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 ⁡ ⋃ dom ⁡ x ∨ Lim ⁡ dom ⁡ x ∧ y = ⋃ ran ⁡ x
2 funopab ⊢ Fun ⁡ x y | x = ∅ ∧ y = A ∨ ¬ x = ∅ ∨ Lim ⁡ dom ⁡ x ∧ y = H ⁡ x ⁡ ⋃ dom ⁡ x ∨ Lim ⁡ dom ⁡ x ∧ y = ⋃ ran ⁡ x ↔ ∀ x ∃* y x = ∅ ∧ 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 ⊢ ∃* y x = ∅ ∧ y = A ∨ ¬ x = ∅ ∨ Lim ⁡ dom ⁡ x ∧ y = H ⁡ x ⁡ ⋃ dom ⁡ x ∨ Lim ⁡ dom ⁡ x ∧ y = ⋃ ran ⁡ x
19 2 18 mpgbir ⊢ Fun ⁡ x y | x = ∅ ∧ y = A ∨ ¬ x = ∅ ∨ Lim ⁡ dom ⁡ x ∧ y = H ⁡ x ⁡ ⋃ dom ⁡ x ∨ Lim ⁡ dom ⁡ x ∧ y = ⋃ ran ⁡ x
20 1 funeqi ⊢ Fun ⁡ G ↔ Fun ⁡ x y | x = ∅ ∧ y = A ∨ ¬ x = ∅ ∨ Lim ⁡ dom ⁡ x ∧ y = H ⁡ x ⁡ ⋃ dom ⁡ x ∨ Lim ⁡ dom ⁡ x ∧ y = ⋃ ran ⁡ x
21 19 20 mpbir ⊢ Fun ⁡ G