Theorem tfrlemisucaccv 5880

Description: We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 5887. (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 4193	. . . 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 5879	. . 3 ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) Fn suc z)
9		vex 2554	. . . . . 6 ⊢ u ∈ V
10	9	elsuc 4109	. . . . 5 ⊢ (u ∈ suc z ↔ (u ∈ z ∨ u = z))
11		vex 2554	. . . . . . . . . . 11 ⊢ g ∈ V
12	4, 11	tfrlem3a 5866	. . . . . . . . . 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 492	. . . . . . . . . 10 ⊢ ((φ ∧ (v ∈ On ∧ (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))) → ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u)))
15		simprrl 491	. . . . . . . . . . . 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 4943	. . . . . . . . . . . 12 ⊢ ((g Fn v ∧ g Fn z) → v = z)
18	15, 16, 17	syl2anc 391	. . . . . . . . . . 11 ⊢ ((φ ∧ (v ∈ On ∧ (g Fn v ∧ ∀u ∈ v (g‘u) = (𝐹‘(g ↾ u))))) → v = z)
19	18	raleqdv 2505	. . . . . . . . . 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 2431	. . . . . . . 8 ⊢ (φ → ∀u ∈ z (g‘u) = (𝐹‘(g ↾ u)))
22	21	r19.21bi 2401	. . . . . . 7 ⊢ ((φ ∧ u ∈ z) → (g‘u) = (𝐹‘(g ↾ u)))
23		elirrv 4226	. . . . . . . . . . 11 ⊢ ¬ u ∈ u
24		elequ2 1598	. . . . . . . . . . 11 ⊢ (z = u → (u ∈ z ↔ u ∈ u))
25	23, 24	mtbiri 599	. . . . . . . . . 10 ⊢ (z = u → ¬ u ∈ z)
26	25	necon2ai 2253	. . . . . . . . 9 ⊢ (u ∈ z → z ≠ u)
27	26	adantl 262	. . . . . . . 8 ⊢ ((φ ∧ u ∈ z) → z ≠ u)
28		fvunsng 5300	. . . . . . . 8 ⊢ ((u ∈ V ∧ z ≠ u) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (g‘u))
29	9, 27, 28	sylancr 393	. . . . . . 7 ⊢ ((φ ∧ u ∈ z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (g‘u))
30		eloni 4078	. . . . . . . . . . . 12 ⊢ (z ∈ On → Ord z)
31	1, 30	syl 14	. . . . . . . . . . 11 ⊢ (φ → Ord z)
32		ordelss 4082	. . . . . . . . . . 11 ⊢ ((Ord z ∧ u ∈ z) → u ⊆ z)
33	31, 32	sylan 267	. . . . . . . . . 10 ⊢ ((φ ∧ u ∈ z) → u ⊆ z)
34		resabs1 4583	. . . . . . . . . 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 4226	. . . . . . . . . . . 12 ⊢ ¬ z ∈ z
37		fsnunres 5307	. . . . . . . . . . . 12 ⊢ ((g Fn z ∧ ¬ z ∈ z) → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z) = g)
38	6, 36, 37	sylancl 392	. . . . . . . . . . 11 ⊢ (φ → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z) = g)
39	38	reseq1d 4554	. . . . . . . . . 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 2071	. . . . . . . 8 ⊢ ((φ ∧ u ∈ z) → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u) = (g ↾ u))
42	41	fveq2d 5125	. . . . . . 7 ⊢ ((φ ∧ u ∈ z) → (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)) = (𝐹‘(g ↾ u)))
43	22, 29, 42	3eqtr4d 2079	. . . . . 6 ⊢ ((φ ∧ u ∈ z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))
44	5	tfrlem3-2d 5869	. . . . . . . . . 10 ⊢ (φ → (Fun 𝐹 ∧ (𝐹‘g) ∈ V))
45	44	simprd 107	. . . . . . . . 9 ⊢ (φ → (𝐹‘g) ∈ V)
46		fndm 4941	. . . . . . . . . . . 12 ⊢ (g Fn z → dom g = z)
47	6, 46	syl 14	. . . . . . . . . . 11 ⊢ (φ → dom g = z)
48	47	eleq2d 2104	. . . . . . . . . 10 ⊢ (φ → (z ∈ dom g ↔ z ∈ z))
49	36, 48	mtbiri 599	. . . . . . . . 9 ⊢ (φ → ¬ z ∈ dom g)
50		fsnunfv 5306	. . . . . . . . 9 ⊢ ((z ∈ On ∧ (𝐹‘g) ∈ V ∧ ¬ z ∈ dom g) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘z) = (𝐹‘g))
51	1, 45, 49, 50	syl3anc 1134	. . . . . . . 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 5125	. . . . . . 7 ⊢ ((φ ∧ u = z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = ((g ∪ {⟨z, (𝐹‘g)⟩})‘z))
55		reseq2 4550	. . . . . . . . 9 ⊢ (u = z → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u) = ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ z))
56	55, 38	sylan9eqr 2091	. . . . . . . 8 ⊢ ((φ ∧ u = z) → ((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u) = g)
57	56	fveq2d 5125	. . . . . . 7 ⊢ ((φ ∧ u = z) → (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)) = (𝐹‘g))
58	52, 54, 57	3eqtr4d 2079	. . . . . 6 ⊢ ((φ ∧ u = z) → ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))
59	43, 58	jaodan 709	. . . . 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 2386	. . 3 ⊢ (φ → ∀u ∈ suc z((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u)))
62		fneq2 4931	. . . . 5 ⊢ (w = suc z → ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn w ↔ (g ∪ {⟨z, (𝐹‘g)⟩}) Fn suc z))
63		raleq 2499	. . . . 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 442	. . . 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 2650	. . 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 1132	. 2 ⊢ (φ → ∃w ∈ On ((g ∪ {⟨z, (𝐹‘g)⟩}) Fn w ∧ ∀u ∈ w ((g ∪ {⟨z, (𝐹‘g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹‘g)⟩}) ↾ u))))
67		vex 2554	. . . . . 6 ⊢ z ∈ V
68		opexg 3955	. . . . . 6 ⊢ ((z ∈ V ∧ (𝐹‘g) ∈ V) → ⟨z, (𝐹‘g)⟩ ∈ V)
69	67, 45, 68	sylancr 393	. . . . 5 ⊢ (φ → ⟨z, (𝐹‘g)⟩ ∈ V)
70		snexg 3927	. . . . 5 ⊢ (⟨z, (𝐹‘g)⟩ ∈ V → {⟨z, (𝐹‘g)⟩} ∈ V)
71	69, 70	syl 14	. . . 4 ⊢ (φ → {⟨z, (𝐹‘g)⟩} ∈ V)
72		unexg 4144	. . . 4 ⊢ ((g ∈ V ∧ {⟨z, (𝐹‘g)⟩} ∈ V) → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ V)
73	11, 71, 72	sylancr 393	. . 3 ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ V)
74	4	tfrlem3ag 5865	. . 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 628  ∀wal 1240   = wceq 1242   ∈ wcel 1390  {cab 2023   ≠ wne 2201  ∀wral 2300  ∃wrex 2301  Vcvv 2551   ∪ cun 2909   ⊆ wss 2911  {csn 3367  ⟨cop 3370  Ord word 4065  Oncon0 4066  suc csuc 4068  dom cdm 4288   ↾ cres 4290  Fun wfun 4839   Fn wfn 4840  ‘cfv 4845

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-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-v 2553  df-sbc 2759  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-br 3756  df-opab 3810  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-res 4300  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853

This theorem is referenced by:  tfrlemibacc  5881  tfrlemi14d  5888