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

Theorem tfrlemisucaccv 6022
Description: We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 6029. (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 4281 . . . 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 6021 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧)
9 vex 2615 . . . . . 6 𝑢 ∈ V
109elsuc 4197 . . . . 5 (𝑢 ∈ suc 𝑧 ↔ (𝑢𝑧𝑢 = 𝑧))
11 vex 2615 . . . . . . . . . . 11 𝑔 ∈ V
124, 11tfrlem3a 6007 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
137, 12sylib 120 . . . . . . . . 9 (𝜑 → ∃𝑣 ∈ On (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
14 simprrr 507 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
15 simprrl 506 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑔 Fn 𝑣)
166adantr 270 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑔 Fn 𝑧)
17 fndmu 5068 . . . . . . . . . . . 12 ((𝑔 Fn 𝑣𝑔 Fn 𝑧) → 𝑣 = 𝑧)
1815, 16, 17syl2anc 403 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → 𝑣 = 𝑧)
1918raleqdv 2561 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → (∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))
2014, 19mpbid 145 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ On ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐹‘(𝑔𝑢))))) → ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
2113, 20rexlimddv 2487 . . . . . . . 8 (𝜑 → ∀𝑢𝑧 (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
2221r19.21bi 2455 . . . . . . 7 ((𝜑𝑢𝑧) → (𝑔𝑢) = (𝐹‘(𝑔𝑢)))
23 elirrv 4327 . . . . . . . . . . 11 ¬ 𝑢𝑢
24 elequ2 1643 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝑢𝑧𝑢𝑢))
2523, 24mtbiri 633 . . . . . . . . . 10 (𝑧 = 𝑢 → ¬ 𝑢𝑧)
2625necon2ai 2303 . . . . . . . . 9 (𝑢𝑧𝑧𝑢)
2726adantl 271 . . . . . . . 8 ((𝜑𝑢𝑧) → 𝑧𝑢)
28 fvunsng 5433 . . . . . . . 8 ((𝑢 ∈ V ∧ 𝑧𝑢) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝑔𝑢))
299, 27, 28sylancr 405 . . . . . . 7 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝑔𝑢))
30 eloni 4166 . . . . . . . . . . . 12 (𝑧 ∈ On → Ord 𝑧)
311, 30syl 14 . . . . . . . . . . 11 (𝜑 → Ord 𝑧)
32 ordelss 4170 . . . . . . . . . . 11 ((Ord 𝑧𝑢𝑧) → 𝑢𝑧)
3331, 32sylan 277 . . . . . . . . . 10 ((𝜑𝑢𝑧) → 𝑢𝑧)
34 resabs1 4699 . . . . . . . . . 10 (𝑢𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))
3533, 34syl 14 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))
36 elirrv 4327 . . . . . . . . . . . 12 ¬ 𝑧𝑧
37 fsnunres 5440 . . . . . . . . . . . 12 ((𝑔 Fn 𝑧 ∧ ¬ 𝑧𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) = 𝑔)
386, 36, 37sylancl 404 . . . . . . . . . . 11 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) = 𝑔)
3938reseq1d 4670 . . . . . . . . . 10 (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
4039adantr 270 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
4135, 40eqtr3d 2117 . . . . . . . 8 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = (𝑔𝑢))
4241fveq2d 5257 . . . . . . 7 ((𝜑𝑢𝑧) → (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) = (𝐹‘(𝑔𝑢)))
4322, 29, 423eqtr4d 2125 . . . . . 6 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
445tfrlem3-2d 6009 . . . . . . . . . 10 (𝜑 → (Fun 𝐹 ∧ (𝐹𝑔) ∈ V))
4544simprd 112 . . . . . . . . 9 (𝜑 → (𝐹𝑔) ∈ V)
46 fndm 5066 . . . . . . . . . . . 12 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
476, 46syl 14 . . . . . . . . . . 11 (𝜑 → dom 𝑔 = 𝑧)
4847eleq2d 2152 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ dom 𝑔𝑧𝑧))
4936, 48mtbiri 633 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
50 fsnunfv 5439 . . . . . . . . 9 ((𝑧 ∈ On ∧ (𝐹𝑔) ∈ V ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
511, 45, 49, 50syl3anc 1170 . . . . . . . 8 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
5251adantr 270 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧) = (𝐹𝑔))
53 simpr 108 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → 𝑢 = 𝑧)
5453fveq2d 5257 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑧))
55 reseq2 4666 . . . . . . . . 9 (𝑢 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑧))
5655, 38sylan9eqr 2137 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢) = 𝑔)
5756fveq2d 5257 . . . . . . 7 ((𝜑𝑢 = 𝑧) → (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) = (𝐹𝑔))
5852, 54, 573eqtr4d 2125 . . . . . 6 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
5943, 58jaodan 744 . . . . 5 ((𝜑 ∧ (𝑢𝑧𝑢 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
6010, 59sylan2b 281 . . . 4 ((𝜑𝑢 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
6160ralrimiva 2440 . . 3 (𝜑 → ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))
62 fneq2 5056 . . . . 5 (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ↔ (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧))
63 raleq 2555 . . . . 5 (𝑤 = suc 𝑧 → (∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)) ↔ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
6462, 63anbi12d 457 . . . 4 (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
6564rspcev 2712 . . 3 ((suc 𝑧 ∈ On ∧ ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))) → ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
663, 8, 61, 65syl12anc 1168 . 2 (𝜑 → ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢))))
67 vex 2615 . . . . . 6 𝑧 ∈ V
68 opexg 4019 . . . . . 6 ((𝑧 ∈ V ∧ (𝐹𝑔) ∈ V) → ⟨𝑧, (𝐹𝑔)⟩ ∈ V)
6967, 45, 68sylancr 405 . . . . 5 (𝜑 → ⟨𝑧, (𝐹𝑔)⟩ ∈ V)
70 snexg 3983 . . . . 5 (⟨𝑧, (𝐹𝑔)⟩ ∈ V → {⟨𝑧, (𝐹𝑔)⟩} ∈ V)
7169, 70syl 14 . . . 4 (𝜑 → {⟨𝑧, (𝐹𝑔)⟩} ∈ V)
72 unexg 4232 . . . 4 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐹𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V)
7311, 71, 72sylancr 405 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V)
744tfrlem3ag 6006 . . 3 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
7573, 74syl 14 . 2 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤 ∈ On ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩})‘𝑢) = (𝐹‘((𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ↾ 𝑢)))))
7666, 75mpbird 165 1 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹𝑔)⟩}) ∈ 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  wal 1283   = wceq 1285  wcel 1434  {cab 2069  wne 2249  wral 2353  wrex 2354  Vcvv 2612  cun 2982  wss 2984  {csn 3422  cop 3425  Ord word 4153  Oncon0 4154  suc csuc 4156  dom cdm 4401  cres 4403  Fun wfun 4963   Fn wfn 4964  cfv 4969
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 4000  ax-un 4224  ax-setind 4316
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-v 2614  df-sbc 2827  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-opab 3866  df-tr 3902  df-id 4084  df-iord 4157  df-on 4159  df-suc 4162  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-res 4413  df-iota 4934  df-fun 4971  df-fn 4972  df-fv 4977
This theorem is referenced by:  tfrlemibacc  6023  tfrlemi14d  6030
  Copyright terms: Public domain W3C validator