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

Theorem tfrlemisucaccv 5969
Description: We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 5976. (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 suceloni 4254 . . . 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 5968 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧)
9 vex 2577 . . . . . 6 𝑢 ∈ V
109elsuc 4170 . . . . 5 (𝑢 ∈ suc 𝑧 ↔ (𝑢𝑧𝑢 = 𝑧))
11 vex 2577 . . . . . . . . . . 11 𝑔 ∈ V
124, 11tfrlem3a 5955 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
137, 12sylib 131 . . . . . . . . 9 (𝜑 → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
14 simprrr 500 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
15 simprrl 499 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑔 Fn 𝑣)
166adantr 265 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑔 Fn 𝑧)
17 fndmu 5027 . . . . . . . . . . . 12 ((𝑔 Fn 𝑣𝑔 Fn 𝑧) → 𝑣 = 𝑧)
1815, 16, 17syl2anc 397 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑣 = 𝑧)
1918raleqdv 2528 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → (∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
2014, 19mpbid 139 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
2113, 20rexlimddv 2454 . . . . . . . 8 (𝜑 → ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
2221r19.21bi 2424 . . . . . . 7 ((𝜑𝑢𝑧) → (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
23 elirrv 4299 . . . . . . . . . . 11 ¬ 𝑢𝑢
24 elequ2 1617 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝑢𝑧𝑢𝑢))
2523, 24mtbiri 610 . . . . . . . . . 10 (𝑧 = 𝑢 → ¬ 𝑢𝑧)
2625necon2ai 2274 . . . . . . . . 9 (𝑢𝑧𝑧𝑢)
2726adantl 266 . . . . . . . 8 ((𝜑𝑢𝑧) → 𝑧𝑢)
28 fvunsng 5384 . . . . . . . 8 ((𝑢 ∈ V ∧ 𝑧𝑢) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝑔𝑢))
299, 27, 28sylancr 399 . . . . . . 7 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝑔𝑢))
30 eloni 4139 . . . . . . . . . . . 12 (𝑧 ∈ On → Ord 𝑧)
311, 30syl 14 . . . . . . . . . . 11 (𝜑 → Ord 𝑧)
32 ordelss 4143 . . . . . . . . . . 11 ((Ord 𝑧𝑢𝑧) → 𝑢𝑧)
3331, 32sylan 271 . . . . . . . . . 10 ((𝜑𝑢𝑧) → 𝑢𝑧)
34 resabs1 4667 . . . . . . . . . 10 (𝑢𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))
3533, 34syl 14 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))
36 elirrv 4299 . . . . . . . . . . . 12 ¬ 𝑧𝑧
37 fsnunres 5391 . . . . . . . . . . . 12 ((𝑔 Fn 𝑧 ∧ ¬ 𝑧𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) = 𝑔)
386, 36, 37sylancl 398 . . . . . . . . . . 11 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) = 𝑔)
3938reseq1d 4638 . . . . . . . . . 10 (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
4039adantr 265 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
4135, 40eqtr3d 2090 . . . . . . . 8 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = (𝑔𝑢))
4241fveq2d 5209 . . . . . . 7 ((𝜑𝑢𝑧) → (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) = (𝐹‘(𝑔𝑢)))
4322, 29, 423eqtr4d 2098 . . . . . 6 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
445tfrlem3-2d 5958 . . . . . . . . . 10 (𝜑 → (Fun 𝐹 ∧ (𝐹𝑔) ∈ V))
4544simprd 111 . . . . . . . . 9 (𝜑 → (𝐹𝑔) ∈ V)
46 fndm 5025 . . . . . . . . . . . 12 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
476, 46syl 14 . . . . . . . . . . 11 (𝜑 → dom 𝑔 = 𝑧)
4847eleq2d 2123 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ dom 𝑔𝑧𝑧))
4936, 48mtbiri 610 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
50 fsnunfv 5390 . . . . . . . . 9 ((𝑧 ∈ On ∧ (𝐹𝑔) ∈ V ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
511, 45, 49, 50syl3anc 1146 . . . . . . . 8 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
5251adantr 265 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
53 simpr 107 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → 𝑢 = 𝑧)
5453fveq2d 5209 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧))
55 reseq2 4634 . . . . . . . . 9 (𝑢 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧))
5655, 38sylan9eqr 2110 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = 𝑔)
5756fveq2d 5209 . . . . . . 7 ((𝜑𝑢 = 𝑧) → (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) = (𝐹𝑔))
5852, 54, 573eqtr4d 2098 . . . . . 6 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
5943, 58jaodan 721 . . . . 5 ((𝜑 ∧ (𝑢𝑧𝑢 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
6010, 59sylan2b 275 . . . 4 ((𝜑𝑢 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
6160ralrimiva 2409 . . 3 (𝜑 → ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
62 fneq2 5015 . . . . 5 (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ↔ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧))
63 raleq 2522 . . . . 5 (𝑤 = suc 𝑧 → (∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) ↔ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
6462, 63anbi12d 450 . . . 4 (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
6564rspcev 2673 . . 3 ((suc 𝑧 ∈ On ∧ ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))) → ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
663, 8, 61, 65syl12anc 1144 . 2 (𝜑 → ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
67 vex 2577 . . . . . 6 𝑧 ∈ V
68 opexg 3991 . . . . . 6 ((𝑧 ∈ V ∧ (𝐹𝑔) ∈ V) → ⟨𝑧, (𝐹𝑔)⟩ ∈ V)
6967, 45, 68sylancr 399 . . . . 5 (𝜑 → ⟨𝑧, (𝐹𝑔)⟩ ∈ V)
70 snexg 3963 . . . . 5 (⟨𝑧, (𝐹𝑔)⟩ ∈ V → {⟨𝑧, (𝐹𝑔)⟩} ∈ V)
7169, 70syl 14 . . . 4 (𝜑 → {⟨𝑧, (𝐹𝑔)⟩} ∈ V)
72 unexg 4205 . . . 4 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐹𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V)
7311, 71, 72sylancr 399 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V)
744tfrlem3ag 5954 . . 3 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
7573, 74syl 14 . 2 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
7666, 75mpbird 160 1 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 101  wb 102  wo 639  wal 1257   = wceq 1259  wcel 1409  {cab 2042  wne 2220  wral 2323  wrex 2324  Vcvv 2574  cun 2942  wss 2944  {csn 3402  cop 3405  Ord word 4126  Oncon0 4127  suc csuc 4129  dom cdm 4372  cres 4374  Fun wfun 4923   Fn wfn 4924  cfv 4929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-v 2576  df-sbc 2787  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-suc 4135  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-res 4384  df-iota 4894  df-fun 4931  df-fn 4932  df-fv 4937
This theorem is referenced by:  tfrlemibacc  5970  tfrlemi14d  5977
  Copyright terms: Public domain W3C validator