Theorem tfrlem7 3919

Description: Lemma for transfinite recursion. The union of all acceptable functions is a function.

Hypotheses

Ref	Expression
tfrlem.1	⊢ A = {f∣∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}
tfrlem.2	⊢ F = ∪A

Assertion

Ref	Expression
tfrlem7	⊢ Fun F

Distinct variable groups:   x,y,f,A   x,F,y,f   x,G,y,f

Proof of Theorem tfrlem7

Step	Hyp	Ref	Expression
1		dffun4 3530	. 2 ⊢ (Fun F ↔ (Rel F ⋀ ∀x∀u∀v((⟨x, u⟩ ∈ F ⋀ ⟨x, v⟩ ∈ F) → u = v)))
2		tfrlem.1	. . 3 ⊢ A = {f∣∃x ∈ On (f Fn x ⋀ ∀y ∈ x (f ‘y) = (G ‘(f ↾ y)))}
3		tfrlem.2	. . 3 ⊢ F = ∪A
4	2, 3	tfrlem6 3918	. 2 ⊢ Rel F
5	3	eleq2i 1535	. . . . . . . 8 ⊢ (⟨x, u⟩ ∈ F ↔ ⟨x, u⟩ ∈ ∪A)
6		eluni 2502	. . . . . . . 8 ⊢ (⟨x, u⟩ ∈ ∪A ↔ ∃g(⟨x, u⟩ ∈ g ⋀ g ∈ A))
7	5, 6	bitr 173	. . . . . . 7 ⊢ (⟨x, u⟩ ∈ F ↔ ∃g(⟨x, u⟩ ∈ g ⋀ g ∈ A))
8	3	eleq2i 1535	. . . . . . . 8 ⊢ (⟨x, v⟩ ∈ F ↔ ⟨x, v⟩ ∈ ∪A)
9		eluni 2502	. . . . . . . 8 ⊢ (⟨x, v⟩ ∈ ∪A ↔ ∃h(⟨x, v⟩ ∈ h ⋀ h ∈ A))
10	8, 9	bitr 173	. . . . . . 7 ⊢ (⟨x, v⟩ ∈ F ↔ ∃h(⟨x, v⟩ ∈ h ⋀ h ∈ A))
11	7, 10	anbi12i 482	. . . . . 6 ⊢ ((⟨x, u⟩ ∈ F ⋀ ⟨x, v⟩ ∈ F) ↔ (∃g(⟨x, u⟩ ∈ g ⋀ g ∈ A) ⋀ ∃h(⟨x, v⟩ ∈ h ⋀ h ∈ A)))
12		eeanv 1321	. . . . . 6 ⊢ (∃g∃h((⟨x, u⟩ ∈ g ⋀ g ∈ A) ⋀ (⟨x, v⟩ ∈ h ⋀ h ∈ A)) ↔ (∃g(⟨x, u⟩ ∈ g ⋀ g ∈ A) ⋀ ∃h(⟨x, v⟩ ∈ h ⋀ h ∈ A)))
13	11, 12	bitr4 176	. . . . 5 ⊢ ((⟨x, u⟩ ∈ F ⋀ ⟨x, v⟩ ∈ F) ↔ ∃g∃h((⟨x, u⟩ ∈ g ⋀ g ∈ A) ⋀ (⟨x, v⟩ ∈ h ⋀ h ∈ A)))
14		an4 506	. . . . . . . 8 ⊢ (((⟨x, u⟩ ∈ g ⋀ g ∈ A) ⋀ (⟨x, v⟩ ∈ h ⋀ h ∈ A)) ↔ ((⟨x, u⟩ ∈ g ⋀ ⟨x, v⟩ ∈ h) ⋀ (g ∈ A ⋀ h ∈ A)))
15		ancom 435	. . . . . . . 8 ⊢ (((⟨x, u⟩ ∈ g ⋀ ⟨x, v⟩ ∈ h) ⋀ (g ∈ A ⋀ h ∈ A)) ↔ ((g ∈ A ⋀ h ∈ A) ⋀ (⟨x, u⟩ ∈ g ⋀ ⟨x, v⟩ ∈ h)))
16	14, 15	bitr 173	. . . . . . 7 ⊢ (((⟨x, u⟩ ∈ g ⋀ g ∈ A) ⋀ (⟨x, v⟩ ∈ h ⋀ h ∈ A)) ↔ ((g ∈ A ⋀ h ∈ A) ⋀ (⟨x, u⟩ ∈ g ⋀ ⟨x, v⟩ ∈ h)))
17	2, 3	tfrlem5 3917	. . . . . . . 8 ⊢ ((g ∈ A ⋀ h ∈ A) → ((⟨x, u⟩ ∈ g ⋀ ⟨x, v⟩ ∈ h) → u = v))
18	17	imp 350	. . . . . . 7 ⊢ (((g ∈ A ⋀ h ∈ A) ⋀ (⟨x, u⟩ ∈ g ⋀ ⟨x, v⟩ ∈ h)) → u = v)
19	16, 18	sylbi 199	. . . . . 6 ⊢ (((⟨x, u⟩ ∈ g ⋀ g ∈ A) ⋀ (⟨x, v⟩ ∈ h ⋀ h ∈ A)) → u = v)
20	19	19.23aivv 1294	. . . . 5 ⊢ (∃g∃h((⟨x, u⟩ ∈ g ⋀ g ∈ A) ⋀ (⟨x, v⟩ ∈ h ⋀ h ∈ A)) → u = v)
21	13, 20	sylbi 199	. . . 4 ⊢ ((⟨x, u⟩ ∈ F ⋀ ⟨x, v⟩ ∈ F) → u = v)
22	21	ax-gen 961	. . 3 ⊢ ∀v((⟨x, u⟩ ∈ F ⋀ ⟨x, v⟩ ∈ F) → u = v)
23	22	gen2 981	. 2 ⊢ ∀x∀u∀v((⟨x, u⟩ ∈ F ⋀ ⟨x, v⟩ ∈ F) → u = v)
24	1, 4, 23	mpbir2an 729	1 ⊢ Fun F

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  {cab 1461  ∀wral 1642  ∃wrex 1643  ⟨cop 2407  ∪cuni 2499  Oncon0 2947   ↾ cres 3172  Rel wrel 3175  Fun wfun 3176   Fn wfn 3177   ‘cfv 3182

This theorem is referenced by:  tfrlem9 3921  tfrlem10 3922  tfr1 3926  numthlem 4775  zorn2lem1 4780  zorn2lem2 4781  zorn2lem5 4784  zorn2lem7 4786

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2699  ax-pow 2738  ax-pr 2775  ax-un 2865

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-rab 1649  df-v 1808  df-sbc 1938  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2500  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2829  df-id 2832  df-po 2839  df-so 2849  df-fr 2916  df-we 2933  df-ord 2950  df-on 2951  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-fv 3198

Copyright terms: Public domain