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

Theorem tfrlemisucaccv 6319
Description: We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 6326. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
Hypotheses
Ref Expression
tfrlemisucfn.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
tfrlemisucfn.2 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
tfrlemisucfn.3 (𝜑𝑧 ∈ On)
tfrlemisucfn.4 (𝜑𝑔 Fn 𝑧)
tfrlemisucfn.5 (𝜑𝑔𝐴)
Assertion
Ref Expression
tfrlemisucaccv (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴)
Distinct variable groups:   𝑓,𝑔,𝑥,𝑦,𝑧,𝐴   𝑓,𝐹,𝑔,𝑥,𝑦,𝑧   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑧,𝑓,𝑔)

Proof of Theorem tfrlemisucaccv
Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrlemisucfn.3 . . . 4 (𝜑𝑧 ∈ On)
2 onsuc 4496 . . . 4 (𝑧 ∈ On → suc 𝑧 ∈ On)
31, 2syl 14 . . 3 (𝜑 → suc 𝑧 ∈ On)
4 tfrlemisucfn.1 . . . 4 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
5 tfrlemisucfn.2 . . . 4 (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹𝑥) ∈ V))
6 tfrlemisucfn.4 . . . 4 (𝜑𝑔 Fn 𝑧)
7 tfrlemisucfn.5 . . . 4 (𝜑𝑔𝐴)
84, 5, 1, 6, 7tfrlemisucfn 6318 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧)
9 vex 2740 . . . . . 6 𝑢 ∈ V
109elsuc 4402 . . . . 5 (𝑢 ∈ suc 𝑧 ↔ (𝑢𝑧𝑢 = 𝑧))
11 vex 2740 . . . . . . . . . . 11 𝑔 ∈ V
124, 11tfrlem3a 6304 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
137, 12sylib 122 . . . . . . . . 9 (𝜑 → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
14 simprrr 540 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
15 simprrl 539 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑔 Fn 𝑣)
166adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑔 Fn 𝑧)
17 fndmu 5312 . . . . . . . . . . . 12 ((𝑔 Fn 𝑣𝑔 Fn 𝑧) → 𝑣 = 𝑧)
1815, 16, 17syl2anc 411 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑣 = 𝑧)
1918raleqdv 2678 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → (∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
2014, 19mpbid 147 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
2113, 20rexlimddv 2599 . . . . . . . 8 (𝜑 → ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
2221r19.21bi 2565 . . . . . . 7 ((𝜑𝑢𝑧) → (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
23 elirrv 4543 . . . . . . . . . . 11 ¬ 𝑢𝑢
24 elequ2 2153 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝑢𝑧𝑢𝑢))
2523, 24mtbiri 675 . . . . . . . . . 10 (𝑧 = 𝑢 → ¬ 𝑢𝑧)
2625necon2ai 2401 . . . . . . . . 9 (𝑢𝑧𝑧𝑢)
2726adantl 277 . . . . . . . 8 ((𝜑𝑢𝑧) → 𝑧𝑢)
28 fvunsng 5705 . . . . . . . 8 ((𝑢 ∈ V ∧ 𝑧𝑢) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝑔𝑢))
299, 27, 28sylancr 414 . . . . . . 7 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝑔𝑢))
30 eloni 4371 . . . . . . . . . . . 12 (𝑧 ∈ On → Ord 𝑧)
311, 30syl 14 . . . . . . . . . . 11 (𝜑 → Ord 𝑧)
32 ordelss 4375 . . . . . . . . . . 11 ((Ord 𝑧𝑢𝑧) → 𝑢𝑧)
3331, 32sylan 283 . . . . . . . . . 10 ((𝜑𝑢𝑧) → 𝑢𝑧)
34 resabs1 4931 . . . . . . . . . 10 (𝑢𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))
3533, 34syl 14 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))
36 elirrv 4543 . . . . . . . . . . . 12 ¬ 𝑧𝑧
37 fsnunres 5713 . . . . . . . . . . . 12 ((𝑔 Fn 𝑧 ∧ ¬ 𝑧𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) = 𝑔)
386, 36, 37sylancl 413 . . . . . . . . . . 11 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) = 𝑔)
3938reseq1d 4901 . . . . . . . . . 10 (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
4039adantr 276 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
4135, 40eqtr3d 2212 . . . . . . . 8 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = (𝑔𝑢))
4241fveq2d 5514 . . . . . . 7 ((𝜑𝑢𝑧) → (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) = (𝐹‘(𝑔𝑢)))
4322, 29, 423eqtr4d 2220 . . . . . 6 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
445tfrlem3-2d 6306 . . . . . . . . . 10 (𝜑 → (Fun 𝐹 ∧ (𝐹𝑔) ∈ V))
4544simprd 114 . . . . . . . . 9 (𝜑 → (𝐹𝑔) ∈ V)
46 fndm 5310 . . . . . . . . . . . 12 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
476, 46syl 14 . . . . . . . . . . 11 (𝜑 → dom 𝑔 = 𝑧)
4847eleq2d 2247 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ dom 𝑔𝑧𝑧))
4936, 48mtbiri 675 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
50 fsnunfv 5712 . . . . . . . . 9 ((𝑧 ∈ On ∧ (𝐹𝑔) ∈ V ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
511, 45, 49, 50syl3anc 1238 . . . . . . . 8 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
5251adantr 276 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
53 simpr 110 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → 𝑢 = 𝑧)
5453fveq2d 5514 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧))
55 reseq2 4897 . . . . . . . . 9 (𝑢 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧))
5655, 38sylan9eqr 2232 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = 𝑔)
5756fveq2d 5514 . . . . . . 7 ((𝜑𝑢 = 𝑧) → (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) = (𝐹𝑔))
5852, 54, 573eqtr4d 2220 . . . . . 6 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
5943, 58jaodan 797 . . . . 5 ((𝜑 ∧ (𝑢𝑧𝑢 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
6010, 59sylan2b 287 . . . 4 ((𝜑𝑢 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
6160ralrimiva 2550 . . 3 (𝜑 → ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
62 fneq2 5300 . . . . 5 (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ↔ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧))
63 raleq 2672 . . . . 5 (𝑤 = suc 𝑧 → (∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) ↔ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
6462, 63anbi12d 473 . . . 4 (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
6564rspcev 2841 . . 3 ((suc 𝑧 ∈ On ∧ ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))) → ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
663, 8, 61, 65syl12anc 1236 . 2 (𝜑 → ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
67 vex 2740 . . . . . 6 𝑧 ∈ V
68 opexg 4224 . . . . . 6 ((𝑧 ∈ V ∧ (𝐹𝑔) ∈ V) → ⟨𝑧, (𝐹𝑔)⟩ ∈ V)
6967, 45, 68sylancr 414 . . . . 5 (𝜑 → ⟨𝑧, (𝐹𝑔)⟩ ∈ V)
70 snexg 4181 . . . . 5 (⟨𝑧, (𝐹𝑔)⟩ ∈ V → {⟨𝑧, (𝐹𝑔)⟩} ∈ V)
7169, 70syl 14 . . . 4 (𝜑 → {⟨𝑧, (𝐹𝑔)⟩} ∈ V)
72 unexg 4439 . . . 4 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐹𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V)
7311, 71, 72sylancr 414 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V)
744tfrlem3ag 6303 . . 3 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
7573, 74syl 14 . 2 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
7666, 75mpbird 167 1 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  wal 1351   = wceq 1353  wcel 2148  {cab 2163  wne 2347  wral 2455  wrex 2456  Vcvv 2737  cun 3127  wss 3129  {csn 3591  cop 3594  Ord word 4358  Oncon0 4359  suc csuc 4361  dom cdm 4622  cres 4624  Fun wfun 5205   Fn wfn 5206  cfv 5211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205  ax-un 4429  ax-setind 4532
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-tr 4099  df-id 4289  df-iord 4362  df-on 4364  df-suc 4367  df-xp 4628  df-rel 4629  df-cnv 4630  df-co 4631  df-dm 4632  df-res 4634  df-iota 5173  df-fun 5213  df-fn 5214  df-fv 5219
This theorem is referenced by:  tfrlemibacc  6320  tfrlemi14d  6327
  Copyright terms: Public domain W3C validator