Theorem tfrlemi14d 5868

Description: The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 9-Jul-2019.)

Hypotheses

Ref	Expression
tfrlemi14d.1	⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}
tfrlemi14d.2	⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))

Assertion

Ref	Expression
tfrlemi14d	⊢ (φ → dom recs(𝐹) = On)

Distinct variable groups:   x,f,y,A   f,𝐹,x,y   φ,f,y

Allowed substitution hint:   φ(x)

Proof of Theorem tfrlemi14d

Dummy variables g ℎ u w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfrlemi14d.1	. . . 4 ⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}
2	1	tfrlem8 5856	. . 3 ⊢ Ord dom recs(𝐹)
3		ordsson 4168	. . 3 ⊢ (Ord dom recs(𝐹) → dom recs(𝐹) ⊆ On)
4	2, 3	mp1i 10	. 2 ⊢ (φ → dom recs(𝐹) ⊆ On)
5		tfrlemi14d.2	. . . . . . . 8 ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))
6	1, 5	tfrlemi1 5867	. . . . . . 7 ⊢ ((φ ∧ z ∈ On) → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))
7	5	ad2antrr 460	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))
8		simplr 470	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → z ∈ On)
9		simprl 471	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → g Fn z)
10		fneq2 4914	. . . . . . . . . . . . 13 ⊢ (w = z → (g Fn w ↔ g Fn z))
11		raleq 2483	. . . . . . . . . . . . 13 ⊢ (w = z → (∀u ∈ w (g‘u) = (𝐹‘(g ↾ u)) ↔ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))
12	10, 11	anbi12d 445	. . . . . . . . . . . 12 ⊢ (w = z → ((g Fn w ∧ ∀u ∈ w (g‘u) = (𝐹‘(g ↾ u))) ↔ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))))
13	12	rspcev 2633	. . . . . . . . . . 11 ⊢ ((z ∈ On ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → ∃w ∈ On (g Fn w ∧ ∀u ∈ w (g‘u) = (𝐹‘(g ↾ u))))
14	13	adantll 448	. . . . . . . . . 10 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → ∃w ∈ On (g Fn w ∧ ∀u ∈ w (g‘u) = (𝐹‘(g ↾ u))))
15		vex 2538	. . . . . . . . . . 11 ⊢ g ∈ V
16	1, 15	tfrlem3a 5847	. . . . . . . . . 10 ⊢ (g ∈ A ↔ ∃w ∈ On (g Fn w ∧ ∀u ∈ w (g‘u) = (𝐹‘(g ↾ u))))
17	14, 16	sylibr 137	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → g ∈ A)
18	1, 7, 8, 9, 17	tfrlemisucaccv 5860	. . . . . . . 8 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A)
19		vex 2538	. . . . . . . . . . . 12 ⊢ z ∈ V
20	5	tfrlem3-2d 5850	. . . . . . . . . . . . 13 ⊢ (φ → (Fun 𝐹 ∧ (𝐹‘g) ∈ V))
21	20	simprd 107	. . . . . . . . . . . 12 ⊢ (φ → (𝐹‘g) ∈ V)
22		opexg 3938	. . . . . . . . . . . 12 ⊢ ((z ∈ V ∧ (𝐹‘g) ∈ V) → ⟨z, (𝐹‘g)⟩ ∈ V)
23	19, 21, 22	sylancr 395	. . . . . . . . . . 11 ⊢ (φ → ⟨z, (𝐹‘g)⟩ ∈ V)
24		snidg 3375	. . . . . . . . . . 11 ⊢ (⟨z, (𝐹‘g)⟩ ∈ V → ⟨z, (𝐹‘g)⟩ ∈ {⟨z, (𝐹‘g)⟩})
25		elun2 3088	. . . . . . . . . . 11 ⊢ (⟨z, (𝐹‘g)⟩ ∈ {⟨z, (𝐹‘g)⟩} → ⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}))
26	23, 24, 25	3syl 17	. . . . . . . . . 10 ⊢ (φ → ⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}))
27	26	ad2antrr 460	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → ⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}))
28		opeldmg 4467	. . . . . . . . . . 11 ⊢ ((z ∈ V ∧ (𝐹‘g) ∈ V) → (⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}) → z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})))
29	19, 21, 28	sylancr 395	. . . . . . . . . 10 ⊢ (φ → (⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}) → z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})))
30	29	ad2antrr 460	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → (⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}) → z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})))
31	27, 30	mpd 13	. . . . . . . 8 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩}))
32		dmeq 4462	. . . . . . . . . 10 ⊢ (ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}) → dom ℎ = dom (g ∪ {⟨z, (𝐹‘g)⟩}))
33	32	eleq2d 2089	. . . . . . . . 9 ⊢ (ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}) → (z ∈ dom ℎ ↔ z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})))
34	33	rspcev 2633	. . . . . . . 8 ⊢ (((g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A ∧ z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})) → ∃ℎ ∈ A z ∈ dom ℎ)
35	18, 31, 34	syl2anc 393	. . . . . . 7 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → ∃ℎ ∈ A z ∈ dom ℎ)
36	6, 35	exlimddv 1760	. . . . . 6 ⊢ ((φ ∧ z ∈ On) → ∃ℎ ∈ A z ∈ dom ℎ)
37		eliun 3635	. . . . . 6 ⊢ (z ∈ ∪ ℎ ∈ A dom ℎ ↔ ∃ℎ ∈ A z ∈ dom ℎ)
38	36, 37	sylibr 137	. . . . 5 ⊢ ((φ ∧ z ∈ On) → z ∈ ∪ ℎ ∈ A dom ℎ)
39	38	ex 108	. . . 4 ⊢ (φ → (z ∈ On → z ∈ ∪ ℎ ∈ A dom ℎ))
40	39	ssrdv 2928	. . 3 ⊢ (φ → On ⊆ ∪ ℎ ∈ A dom ℎ)
41	1	recsfval 5853	. . . . 5 ⊢ recs(𝐹) = ∪ A
42	41	dmeqi 4463	. . . 4 ⊢ dom recs(𝐹) = dom ∪ A
43		dmuni 4472	. . . 4 ⊢ dom ∪ A = ∪ ℎ ∈ A dom ℎ
44	42, 43	eqtri 2042	. . 3 ⊢ dom recs(𝐹) = ∪ ℎ ∈ A dom ℎ
45	40, 44	syl6sseqr 2969	. 2 ⊢ (φ → On ⊆ dom recs(𝐹))
46	4, 45	eqssd 2939	1 ⊢ (φ → dom recs(𝐹) = On)

Syntax hints:   → wi 4   ∧ wa 97  ∀wal 1226   = wceq 1228   ∈ wcel 1374  {cab 2008  ∀wral 2284  ∃wrex 2285  Vcvv 2535   ∪ cun 2892   ⊆ wss 2894  {csn 3350  ⟨cop 3353  ∪ cuni 3554  ∪ ciun 3631  Ord word 4048  Oncon0 4049  dom cdm 4272   ↾ cres 4274  Fun wfun 4823   Fn wfn 4824  ‘cfv 4829  recscrecs 5841

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-coll 3846  ax-sep 3849  ax-pow 3901  ax-pr 3918  ax-un 4120  ax-setind 4204

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-reu 2291  df-rab 2293  df-v 2537  df-sbc 2742  df-csb 2830  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-iun 3633  df-br 3739  df-opab 3793  df-mpt 3794  df-tr 3829  df-id 4004  df-iord 4052  df-on 4054  df-suc 4057  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-rn 4283  df-res 4284  df-ima 4285  df-iota 4794  df-fun 4831  df-fn 4832  df-f 4833  df-f1 4834  df-fo 4835  df-f1o 4836  df-fv 4837  df-recs 5842

This theorem is referenced by:  tfri1d  5871