Theorem tz7.44lem1

Description: G is a function. Lemma for tz7.44-1 , tz7.44-2 , and tz7.44-3 . (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 𝐺