ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tfrlemisucaccv Structured version   GIF version

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 = {fx On (f Fn x y x (fy) = (𝐹‘(fy)))}
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.
StepHypRef Expression
1 tfrlemisucfn.3 . . . 4 (φz On)
2 suceloni 4177 . . . 4 (z On → suc z On)
31, 2syl 14 . . 3 (φ → suc z On)
4 tfrlemisucfn.1 . . . 4 A = {fx On (f Fn x y x (fy) = (𝐹‘(fy)))}
5 tfrlemisucfn.2 . . . 4 (φx(Fun 𝐹 (𝐹x) V))
6 tfrlemisucfn.4 . . . 4 (φg Fn z)
7 tfrlemisucfn.5 . . . 4 (φg A)
84, 5, 1, 6, 7tfrlemisucfn 5859 . . 3 (φ → (g ∪ {⟨z, (𝐹g)⟩}) Fn suc z)
9 vex 2538 . . . . . 6 u V
109elsuc 4092 . . . . 5 (u suc z ↔ (u z u = z))
11 vex 2538 . . . . . . . . . . 11 g V
124, 11tfrlem3a 5847 . . . . . . . . . 10 (g Av On (g Fn v u v (gu) = (𝐹‘(gu))))
137, 12sylib 127 . . . . . . . . 9 (φv On (g Fn v u v (gu) = (𝐹‘(gu))))
14 simprrr 480 . . . . . . . . . 10 ((φ (v On (g Fn v u v (gu) = (𝐹‘(gu))))) → u v (gu) = (𝐹‘(gu)))
15 simprrl 479 . . . . . . . . . . . 12 ((φ (v On (g Fn v u v (gu) = (𝐹‘(gu))))) → g Fn v)
166adantr 261 . . . . . . . . . . . 12 ((φ (v On (g Fn v u v (gu) = (𝐹‘(gu))))) → g Fn z)
17 fndmu 4926 . . . . . . . . . . . 12 ((g Fn v g Fn z) → v = z)
1815, 16, 17syl2anc 393 . . . . . . . . . . 11 ((φ (v On (g Fn v u v (gu) = (𝐹‘(gu))))) → v = z)
1918raleqdv 2489 . . . . . . . . . 10 ((φ (v On (g Fn v u v (gu) = (𝐹‘(gu))))) → (u v (gu) = (𝐹‘(gu)) ↔ u z (gu) = (𝐹‘(gu))))
2014, 19mpbid 135 . . . . . . . . 9 ((φ (v On (g Fn v u v (gu) = (𝐹‘(gu))))) → u z (gu) = (𝐹‘(gu)))
2113, 20rexlimddv 2415 . . . . . . . 8 (φu z (gu) = (𝐹‘(gu)))
2221r19.21bi 2385 . . . . . . 7 ((φ u z) → (gu) = (𝐹‘(gu)))
23 elirrv 4210 . . . . . . . . . . 11 ¬ u u
24 elequ2 1583 . . . . . . . . . . 11 (z = u → (u zu u))
2523, 24mtbiri 587 . . . . . . . . . 10 (z = u → ¬ u z)
2625necon2ai 2237 . . . . . . . . 9 (u zzu)
2726adantl 262 . . . . . . . 8 ((φ u z) → zu)
28 fvunsng 5282 . . . . . . . 8 ((u V zu) → ((g ∪ {⟨z, (𝐹g)⟩})‘u) = (gu))
299, 27, 28sylancr 395 . . . . . . 7 ((φ u z) → ((g ∪ {⟨z, (𝐹g)⟩})‘u) = (gu))
30 eloni 4061 . . . . . . . . . . . 12 (z On → Ord z)
311, 30syl 14 . . . . . . . . . . 11 (φ → Ord z)
32 ordelss 4065 . . . . . . . . . . 11 ((Ord z u z) → uz)
3331, 32sylan 267 . . . . . . . . . 10 ((φ u z) → uz)
34 resabs1 4567 . . . . . . . . . 10 (uz → (((g ∪ {⟨z, (𝐹g)⟩}) ↾ z) ↾ u) = ((g ∪ {⟨z, (𝐹g)⟩}) ↾ u))
3533, 34syl 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)
386, 36, 37sylancl 394 . . . . . . . . . . 11 (φ → ((g ∪ {⟨z, (𝐹g)⟩}) ↾ z) = g)
3938reseq1d 4538 . . . . . . . . . 10 (φ → (((g ∪ {⟨z, (𝐹g)⟩}) ↾ z) ↾ u) = (gu))
4039adantr 261 . . . . . . . . 9 ((φ u z) → (((g ∪ {⟨z, (𝐹g)⟩}) ↾ z) ↾ u) = (gu))
4135, 40eqtr3d 2056 . . . . . . . 8 ((φ u z) → ((g ∪ {⟨z, (𝐹g)⟩}) ↾ u) = (gu))
4241fveq2d 5107 . . . . . . 7 ((φ u z) → (𝐹‘((g ∪ {⟨z, (𝐹g)⟩}) ↾ u)) = (𝐹‘(gu)))
4322, 29, 423eqtr4d 2064 . . . . . 6 ((φ u z) → ((g ∪ {⟨z, (𝐹g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹g)⟩}) ↾ u)))
445tfrlem3-2d 5850 . . . . . . . . . 10 (φ → (Fun 𝐹 (𝐹g) V))
4544simprd 107 . . . . . . . . 9 (φ → (𝐹g) V)
46 fndm 4924 . . . . . . . . . . . 12 (g Fn z → dom g = z)
476, 46syl 14 . . . . . . . . . . 11 (φ → dom g = z)
4847eleq2d 2089 . . . . . . . . . 10 (φ → (z dom gz z))
4936, 48mtbiri 587 . . . . . . . . 9 (φ → ¬ z dom g)
50 fsnunfv 5288 . . . . . . . . 9 ((z On (𝐹g) V ¬ z dom g) → ((g ∪ {⟨z, (𝐹g)⟩})‘z) = (𝐹g))
511, 45, 49, 50syl3anc 1121 . . . . . . . 8 (φ → ((g ∪ {⟨z, (𝐹g)⟩})‘z) = (𝐹g))
5251adantr 261 . . . . . . 7 ((φ u = z) → ((g ∪ {⟨z, (𝐹g)⟩})‘z) = (𝐹g))
53 simpr 103 . . . . . . . 8 ((φ u = z) → u = z)
5453fveq2d 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))
5655, 38sylan9eqr 2076 . . . . . . . 8 ((φ u = z) → ((g ∪ {⟨z, (𝐹g)⟩}) ↾ u) = g)
5756fveq2d 5107 . . . . . . 7 ((φ u = z) → (𝐹‘((g ∪ {⟨z, (𝐹g)⟩}) ↾ u)) = (𝐹g))
5852, 54, 573eqtr4d 2064 . . . . . 6 ((φ u = z) → ((g ∪ {⟨z, (𝐹g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹g)⟩}) ↾ u)))
5943, 58jaodan 697 . . . . 5 ((φ (u z u = z)) → ((g ∪ {⟨z, (𝐹g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹g)⟩}) ↾ u)))
6010, 59sylan2b 271 . . . 4 ((φ u suc z) → ((g ∪ {⟨z, (𝐹g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹g)⟩}) ↾ u)))
6160ralrimiva 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))))
6462, 63anbi12d 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)))))
6564rspcev 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))))
663, 8, 61, 65syl12anc 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)
6967, 45, 68sylancr 395 . . . . 5 (φ → ⟨z, (𝐹g)⟩ V)
70 snexg 3910 . . . . 5 (⟨z, (𝐹g)⟩ V → {⟨z, (𝐹g)⟩} V)
7169, 70syl 14 . . . 4 (φ → {⟨z, (𝐹g)⟩} V)
72 unexg 4128 . . . 4 ((g V {⟨z, (𝐹g)⟩} V) → (g ∪ {⟨z, (𝐹g)⟩}) V)
7311, 71, 72sylancr 395 . . 3 (φ → (g ∪ {⟨z, (𝐹g)⟩}) V)
744tfrlem3ag 5846 . . 3 ((g ∪ {⟨z, (𝐹g)⟩}) V → ((g ∪ {⟨z, (𝐹g)⟩}) Aw On ((g ∪ {⟨z, (𝐹g)⟩}) Fn w u w ((g ∪ {⟨z, (𝐹g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹g)⟩}) ↾ u)))))
7573, 74syl 14 . 2 (φ → ((g ∪ {⟨z, (𝐹g)⟩}) Aw On ((g ∪ {⟨z, (𝐹g)⟩}) Fn w u w ((g ∪ {⟨z, (𝐹g)⟩})‘u) = (𝐹‘((g ∪ {⟨z, (𝐹g)⟩}) ↾ u)))))
7666, 75mpbird 156 1 (φ → (g ∪ {⟨z, (𝐹g)⟩}) A)
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator