Theorem tfrlemi14d 5888

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 5875	. . 3 ⊢ Ord dom recs(𝐹)
3		ordsson 4184	. . 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 5887	. . . . . . 7 ⊢ ((φ ∧ z ∈ On) → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))
7	5	ad2antrr 457	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))
8		simplr 482	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → z ∈ On)
9		simprl 483	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → g Fn z)
10		fneq2 4931	. . . . . . . . . . . . 13 ⊢ (w = z → (g Fn w ↔ g Fn z))
11		raleq 2499	. . . . . . . . . . . . 13 ⊢ (w = z → (∀u ∈ w (g‘u) = (𝐹‘(g ↾ u)) ↔ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))
12	10, 11	anbi12d 442	. . . . . . . . . . . 12 ⊢ (w = z → ((g Fn w ∧ ∀u ∈ w (g‘u) = (𝐹‘(g ↾ u))) ↔ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))))
13	12	rspcev 2650	. . . . . . . . . . 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 445	. . . . . . . . . 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 2554	. . . . . . . . . . 11 ⊢ g ∈ V
16	1, 15	tfrlem3a 5866	. . . . . . . . . 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 5880	. . . . . . . 8 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A)
19		vex 2554	. . . . . . . . . . . 12 ⊢ z ∈ V
20	5	tfrlem3-2d 5869	. . . . . . . . . . . . 13 ⊢ (φ → (Fun 𝐹 ∧ (𝐹‘g) ∈ V))
21	20	simprd 107	. . . . . . . . . . . 12 ⊢ (φ → (𝐹‘g) ∈ V)
22		opexg 3955	. . . . . . . . . . . 12 ⊢ ((z ∈ V ∧ (𝐹‘g) ∈ V) → ⟨z, (𝐹‘g)⟩ ∈ V)
23	19, 21, 22	sylancr 393	. . . . . . . . . . 11 ⊢ (φ → ⟨z, (𝐹‘g)⟩ ∈ V)
24		snidg 3392	. . . . . . . . . . 11 ⊢ (⟨z, (𝐹‘g)⟩ ∈ V → ⟨z, (𝐹‘g)⟩ ∈ {⟨z, (𝐹‘g)⟩})
25		elun2 3105	. . . . . . . . . . 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 457	. . . . . . . . 9 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → ⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}))
28		opeldmg 4483	. . . . . . . . . . 11 ⊢ ((z ∈ V ∧ (𝐹‘g) ∈ V) → (⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}) → z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})))
29	19, 21, 28	sylancr 393	. . . . . . . . . 10 ⊢ (φ → (⟨z, (𝐹‘g)⟩ ∈ (g ∪ {⟨z, (𝐹‘g)⟩}) → z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})))
30	29	ad2antrr 457	. . . . . . . . 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 4478	. . . . . . . . . 10 ⊢ (ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}) → dom ℎ = dom (g ∪ {⟨z, (𝐹‘g)⟩}))
33	32	eleq2d 2104	. . . . . . . . 9 ⊢ (ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}) → (z ∈ dom ℎ ↔ z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})))
34	33	rspcev 2650	. . . . . . . 8 ⊢ (((g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A ∧ z ∈ dom (g ∪ {⟨z, (𝐹‘g)⟩})) → ∃ℎ ∈ A z ∈ dom ℎ)
35	18, 31, 34	syl2anc 391	. . . . . . 7 ⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))) → ∃ℎ ∈ A z ∈ dom ℎ)
36	6, 35	exlimddv 1775	. . . . . 6 ⊢ ((φ ∧ z ∈ On) → ∃ℎ ∈ A z ∈ dom ℎ)
37		eliun 3652	. . . . . 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 2945	. . 3 ⊢ (φ → On ⊆ ∪ ℎ ∈ A dom ℎ)
41	1	recsfval 5872	. . . . 5 ⊢ recs(𝐹) = ∪ A
42	41	dmeqi 4479	. . . 4 ⊢ dom recs(𝐹) = dom ∪ A
43		dmuni 4488	. . . 4 ⊢ dom ∪ A = ∪ ℎ ∈ A dom ℎ
44	42, 43	eqtri 2057	. . 3 ⊢ dom recs(𝐹) = ∪ ℎ ∈ A dom ℎ
45	40, 44	syl6sseqr 2986	. 2 ⊢ (φ → On ⊆ dom recs(𝐹))
46	4, 45	eqssd 2956	1 ⊢ (φ → dom recs(𝐹) = On)

Syntax hints:   → wi 4   ∧ wa 97  ∀wal 1240   = wceq 1242   ∈ wcel 1390  {cab 2023  ∀wral 2300  ∃wrex 2301  Vcvv 2551   ∪ cun 2909   ⊆ wss 2911  {csn 3367  ⟨cop 3370  ∪ cuni 3571  ∪ ciun 3648  Ord word 4065  Oncon0 4066  dom cdm 4288   ↾ cres 4290  Fun wfun 4839   Fn wfn 4840  ‘cfv 4845  recscrecs 5860

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 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-suc 4074  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-recs 5861

This theorem is referenced by:  tfri1d  5890