Theorem tfrlemisucaccv 5860

Description: We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 5867. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)

Hypotheses

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

Assertion

Ref	Expression
tfrlemisucaccv	⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A)

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

Allowed substitution hints:   φ(x,z,f,g)

Proof of Theorem tfrlemisucaccv

Dummy variables u v w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfrlemisucfn.3	. . . 4 ⊢ (φ → z ∈ On)
2		suceloni 4177	. . . 4 ⊢ (z ∈ On → suc z ∈ On)
3	1, 2	syl 14	. . 3 ⊢ (φ → suc z ∈ On)
4		tfrlemisucfn.1	. . . 4 ⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}
5		tfrlemisucfn.2	. . . 4 ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))
6		tfrlemisucfn.4	. . . 4 ⊢ (φ → g Fn z)
7		tfrlemisucfn.5	. . . 4 ⊢ (φ → g ∈ A)
8	4, 5, 1, 6, 7	tfrlemisucfn 5859	. . 3 ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) Fn suc z)
9		vex 2538	. . . . . 6 ⊢ u ∈ V
10	9	elsuc 4092	. . . . 5 ⊢ (u ∈ suc z ↔ (u ∈ z ∨ u = z))
11		vex 2538	. . . . . . . . . . 11 ⊢ g ∈ V
12	4, 11	tfrlem3a 5847	. . . . . . . . . 10 ⊢ (g ∈ A ↔ ∃v ∈ On (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))
13	7, 12	sylib 127	. . . . . . . . 9 ⊢ (φ → ∃v ∈ On (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))
14		simprrr 480	. . . . . . . . . 10 ⊢ ((φ ∧ (v ∈ On ∧ (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))) → ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u)))
15		simprrl 479	. . . . . . . . . . . 12 ⊢ ((φ ∧ (v ∈ On ∧ (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))) → g Fn v)
16	6	adantr 261	. . . . . . . . . . . 12 ⊢ ((φ ∧ (v ∈ On ∧ (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))) → g Fn z)
17		fndmu 4926	. . . . . . . . . . . 12 ⊢ ((g Fn v ∧ g Fn z) → v = z)
18	15, 16, 17	syl2anc 393	. . . . . . . . . . 11 ⊢ ((φ ∧ (v ∈ On ∧ (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))) → v = z)
19	18	raleqdv 2489	. . . . . . . . . 10 ⊢ ((φ ∧ (v ∈ On ∧ (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))) → (∀u ∈ v (g‘u) = (𝐹‘(g ↾ u)) ↔ ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u))))
20	14, 19	mpbid 135	. . . . . . . . 9 ⊢ ((φ ∧ (v ∈ On ∧ (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))) → ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))
21	13, 20	rexlimddv 2415	. . . . . . . 8 ⊢ (φ → ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))
22	21	r19.21bi 2385	. . . . . . 7 ⊢ ((φ ∧ u ∈ z) → (g‘u) = (𝐹‘(g ↾ u)))
23		elirrv 4210	. . . . . . . . . . 11 ⊢ ¬ u ∈ u
24		elequ2 1583	. . . . . . . . . . 11 ⊢ (z = u → (u ∈ z ↔ u ∈ u))
25	23, 24	mtbiri 587	. . . . . . . . . 10 ⊢ (z = u → ¬ u ∈ z)
26	25	necon2ai 2237	. . . . . . . . 9 ⊢ (u ∈ z → z ≠ u)
27	26	adantl 262	. . . . . . . 8 ⊢ ((φ ∧ u ∈ z) → z ≠ u)
28		fvunsng 5282	. . . . . . . 8 ⊢ ((u ∈ V ∧ z ≠ u) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (g‘u))
29	9, 27, 28	sylancr 395	. . . . . . 7 ⊢ ((φ ∧ u ∈ z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (g‘u))
30		eloni 4061	. . . . . . . . . . . 12 ⊢ (z ∈ On → Ord z)
31	1, 30	syl 14	. . . . . . . . . . 11 ⊢ (φ → Ord z)
32		ordelss 4065	. . . . . . . . . . 11 ⊢ ((Ord z ∧ u ∈ z) → u ⊆ z)
33	31, 32	sylan 267	. . . . . . . . . 10 ⊢ ((φ ∧ u ∈ z) → u ⊆ z)
34		resabs1 4567	. . . . . . . . . 10 ⊢ (u ⊆ z → (((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z) ↾ u) = ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u))
35	33, 34	syl 14	. . . . . . . . 9 ⊢ ((φ ∧ u ∈ z) → (((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z) ↾ u) = ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u))
36		elirrv 4210	. . . . . . . . . . . 12 ⊢ ¬ z ∈ z
37		fsnunres 5289	. . . . . . . . . . . 12 ⊢ ((g Fn z ∧ ¬ z ∈ z) → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z) = g)
38	6, 36, 37	sylancl 394	. . . . . . . . . . 11 ⊢ (φ → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z) = g)
39	38	reseq1d 4538	. . . . . . . . . 10 ⊢ (φ → (((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z) ↾ u) = (g ↾ u))
40	39	adantr 261	. . . . . . . . 9 ⊢ ((φ ∧ u ∈ z) → (((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z) ↾ u) = (g ↾ u))
41	35, 40	eqtr3d 2056	. . . . . . . 8 ⊢ ((φ ∧ u ∈ z) → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u) = (g ↾ u))
42	41	fveq2d 5107	. . . . . . 7 ⊢ ((φ ∧ u ∈ z) → (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)) = (𝐹‘(g ↾ u)))
43	22, 29, 42	3eqtr4d 2064	. . . . . 6 ⊢ ((φ ∧ u ∈ z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))
44	5	tfrlem3-2d 5850	. . . . . . . . . 10 ⊢ (φ → (Fun 𝐹 ∧ (𝐹‘g) ∈ V))
45	44	simprd 107	. . . . . . . . 9 ⊢ (φ → (𝐹‘g) ∈ V)
46		fndm 4924	. . . . . . . . . . . 12 ⊢ (g Fn z → dom g = z)
47	6, 46	syl 14	. . . . . . . . . . 11 ⊢ (φ → dom g = z)
48	47	eleq2d 2089	. . . . . . . . . 10 ⊢ (φ → (z ∈ dom g ↔ z ∈ z))
49	36, 48	mtbiri 587	. . . . . . . . 9 ⊢ (φ → ¬ z ∈ dom g)
50		fsnunfv 5288	. . . . . . . . 9 ⊢ ((z ∈ On ∧ (𝐹‘g) ∈ V ∧ ¬ z ∈ dom g) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘z) = (𝐹‘g))
51	1, 45, 49, 50	syl3anc 1121	. . . . . . . 8 ⊢ (φ → ((g ∪ {⟨z, (𝐹‘g)⟩})‘z) = (𝐹‘g))
52	51	adantr 261	. . . . . . 7 ⊢ ((φ ∧ u = z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘z) = (𝐹‘g))
53		simpr 103	. . . . . . . 8 ⊢ ((φ ∧ u = z) → u = z)
54	53	fveq2d 5107	. . . . . . 7 ⊢ ((φ ∧ u = z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = ((g ∪ {⟨z, (𝐹‘g)⟩})‘z))
55		reseq2 4534	. . . . . . . . 9 ⊢ (u = z → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u) = ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z))
56	55, 38	sylan9eqr 2076	. . . . . . . 8 ⊢ ((φ ∧ u = z) → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u) = g)
57	56	fveq2d 5107	. . . . . . 7 ⊢ ((φ ∧ u = z) → (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)) = (𝐹‘g))
58	52, 54, 57	3eqtr4d 2064	. . . . . 6 ⊢ ((φ ∧ u = z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))
59	43, 58	jaodan 697	. . . . 5 ⊢ ((φ ∧ (u ∈ z ∨ u = z)) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))
60	10, 59	sylan2b 271	. . . 4 ⊢ ((φ ∧ u ∈ suc z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))
61	60	ralrimiva 2370	. . 3 ⊢ (φ → ∀u ∈ suc z((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))
62		fneq2 4914	. . . . 5 ⊢ (w = suc z → ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn w ↔ (g ∪ {⟨z, (𝐹‘g)⟩}) Fn suc z))
63		raleq 2483	. . . . 5 ⊢ (w = suc z → (∀u ∈ w ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)) ↔ ∀u ∈ suc z((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u))))
64	62, 63	anbi12d 445	. . . 4 ⊢ (w = suc z → (((g ∪ {⟨z, (𝐹‘g)⟩}) Fn w ∧ ∀u ∈ w ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u))) ↔ ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn suc z ∧ ∀u ∈ suc z((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))))
65	64	rspcev 2633	. . 3 ⊢ ((suc z ∈ On ∧ ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn suc z ∧ ∀u ∈ suc z((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))) → ∃w ∈ On ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn w ∧ ∀u ∈ w ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u))))
66	3, 8, 61, 65	syl12anc 1119	. 2 ⊢ (φ → ∃w ∈ On ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn w ∧ ∀u ∈ w ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u))))
67		vex 2538	. . . . . 6 ⊢ z ∈ V
68		opexg 3938	. . . . . 6 ⊢ ((z ∈ V ∧ (𝐹‘g) ∈ V) → ⟨z, (𝐹‘g)⟩ ∈ V)
69	67, 45, 68	sylancr 395	. . . . 5 ⊢ (φ → ⟨z, (𝐹‘g)⟩ ∈ V)
70		snexg 3910	. . . . 5 ⊢ (⟨z, (𝐹‘g)⟩ ∈ V → {⟨z, (𝐹‘g)⟩} ∈ V)
71	69, 70	syl 14	. . . 4 ⊢ (φ → {⟨z, (𝐹‘g)⟩} ∈ V)
72		unexg 4128	. . . 4 ⊢ ((g ∈ V ∧ {⟨z, (𝐹‘g)⟩} ∈ V) → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ V)
73	11, 71, 72	sylancr 395	. . 3 ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ V)
74	4	tfrlem3ag 5846	. . 3 ⊢ ((g ∪ {⟨z, (𝐹‘g)⟩}) ∈ V → ((g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A ↔ ∃w ∈ On ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn w ∧ ∀u ∈ w ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))))
75	73, 74	syl 14	. 2 ⊢ (φ → ((g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A ↔ ∃w ∈ On ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn w ∧ ∀u ∈ w ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))))
76	66, 75	mpbird 156	1 ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616  ∀wal 1226   = wceq 1228   ∈ wcel 1374  {cab 2008   ≠ wne 2186  ∀wral 2284  ∃wrex 2285  Vcvv 2535   ∪ cun 2892   ⊆ wss 2894  {csn 3350  ⟨cop 3353  Ord word 4048  Oncon0 4049  suc csuc 4051  dom cdm 4272   ↾ cres 4274  Fun wfun 4823   Fn wfn 4824  ‘cfv 4829

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-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-v 2537  df-sbc 2742  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-br 3739  df-opab 3793  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-res 4284  df-iota 4794  df-fun 4831  df-fn 4832  df-fv 4837

This theorem is referenced by:  tfrlemibacc  5861  tfrlemi14d  5868  tfrlemi14  5869