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 ⊢ 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 = ∅ ∧ 𝑦 = 𝐴 ) ∨ ( ¬ ( 𝑥 = ∅ ∨ Lim dom 𝑥 ) ∧ 𝑦 = ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ∨ ( Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥 ) ) }
Assertion tz7.44lem1 Fun 𝐺

Proof

Step Hyp Ref Expression
1 tz7.44lem1.1 ⊢ 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 = ∅ ∧ 𝑦 = 𝐴 ) ∨ ( ¬ ( 𝑥 = ∅ ∨ Lim dom 𝑥 ) ∧ 𝑦 = ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ∨ ( Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥 ) ) }
2 funopab ⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 = ∅ ∧ 𝑦 = 𝐴 ) ∨ ( ¬ ( 𝑥 = ∅ ∨ Lim dom 𝑥 ) ∧ 𝑦 = ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ∨ ( Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥 ) ) } ↔ ∀ 𝑥 ∃* 𝑦 ( ( 𝑥 = ∅ ∧ 𝑦 = 𝐴 ) ∨ ( ¬ ( 𝑥 = ∅ ∨ Lim dom 𝑥 ) ∧ 𝑦 = ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ∨ ( Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥 ) ) )
3 fvex ⊢ ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∈ V
4 vex ⊢ 𝑥 ∈ V
5 rnexg ⊢ ( 𝑥 ∈ V → ran 𝑥 ∈ V )
6 uniexg ⊢ ( ran 𝑥 ∈ V → ∪ ran 𝑥 ∈ V )
7 4 5 6 mp2b ⊢ ∪ ran 𝑥 ∈ 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 ⊢ ( 𝑥 = ∅ → dom 𝑥 = dom ∅ )
14 limeq ⊢ ( dom 𝑥 = dom ∅ → ( Lim dom 𝑥 ↔ Lim dom ∅ ) )
15 13 14 syl ⊢ ( 𝑥 = ∅ → ( Lim dom 𝑥 ↔ Lim dom ∅ ) )
16 15 biimpa ⊢ ( ( 𝑥 = ∅ ∧ Lim dom 𝑥 ) → Lim dom ∅ )
17 12 16 mto ⊢ ¬ ( 𝑥 = ∅ ∧ Lim dom 𝑥 )
18 3 7 17 moeq3 ⊢ ∃* 𝑦 ( ( 𝑥 = ∅ ∧ 𝑦 = 𝐴 ) ∨ ( ¬ ( 𝑥 = ∅ ∨ Lim dom 𝑥 ) ∧ 𝑦 = ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ∨ ( Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥 ) )
19 2 18 mpgbir ⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 = ∅ ∧ 𝑦 = 𝐴 ) ∨ ( ¬ ( 𝑥 = ∅ ∨ Lim dom 𝑥 ) ∧ 𝑦 = ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ∨ ( Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥 ) ) }
20 1 funeqi ⊢ ( Fun 𝐺 ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 = ∅ ∧ 𝑦 = 𝐴 ) ∨ ( ¬ ( 𝑥 = ∅ ∨ Lim dom 𝑥 ) ∧ 𝑦 = ( 𝐻 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ∨ ( Lim dom 𝑥 ∧ 𝑦 = ∪ ran 𝑥 ) ) } )
21 19 20 mpbir ⊢ Fun 𝐺