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

Theorem tfr1onlemsucaccv 6339
Description: Lemma for tfr1on 6348. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 12-Mar-2022.)
Hypotheses
Ref Expression
tfr1on.f 𝐹 = recs(𝐺)
tfr1on.g (𝜑 → Fun 𝐺)
tfr1on.x (𝜑 → Ord 𝑋)
tfr1on.ex ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
tfr1onlemsucfn.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfr1onlemsucaccv.yx (𝜑𝑌𝑋)
tfr1onlemsucaccv.zy (𝜑𝑧𝑌)
tfr1onlemsucaccv.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
tfr1onlemsucaccv.gfn (𝜑𝑔 Fn 𝑧)
tfr1onlemsucaccv.gacc (𝜑𝑔𝐴)
Assertion
Ref Expression
tfr1onlemsucaccv (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴)
Distinct variable groups:   𝑓,𝐺,𝑥,𝑦   𝑓,𝑋,𝑥   𝑓,𝑔,𝑥,𝑦   𝜑,𝑓,𝑥   𝑧,𝑓,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑦,𝑧,𝑔)   𝐴(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔)   𝐺(𝑧,𝑔)   𝑋(𝑦,𝑧,𝑔)   𝑌(𝑥,𝑦,𝑧,𝑓,𝑔)

Proof of Theorem tfr1onlemsucaccv
Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suceq 4401 . . . . 5 (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧)
21eleq1d 2246 . . . 4 (𝑥 = 𝑧 → (suc 𝑥𝑋 ↔ suc 𝑧𝑋))
3 tfr1onlemsucaccv.u . . . . 5 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
43ralrimiva 2550 . . . 4 (𝜑 → ∀𝑥 𝑋 suc 𝑥𝑋)
5 tfr1onlemsucaccv.zy . . . . 5 (𝜑𝑧𝑌)
6 tfr1onlemsucaccv.yx . . . . 5 (𝜑𝑌𝑋)
7 elunii 3814 . . . . 5 ((𝑧𝑌𝑌𝑋) → 𝑧 𝑋)
85, 6, 7syl2anc 411 . . . 4 (𝜑𝑧 𝑋)
92, 4, 8rspcdva 2846 . . 3 (𝜑 → suc 𝑧𝑋)
10 tfr1on.f . . . 4 𝐹 = recs(𝐺)
11 tfr1on.g . . . 4 (𝜑 → Fun 𝐺)
12 tfr1on.x . . . 4 (𝜑 → Ord 𝑋)
13 tfr1on.ex . . . 4 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
14 tfr1onlemsucfn.1 . . . 4 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
155, 6jca 306 . . . . 5 (𝜑 → (𝑧𝑌𝑌𝑋))
16 ordtr1 4387 . . . . 5 (Ord 𝑋 → ((𝑧𝑌𝑌𝑋) → 𝑧𝑋))
1712, 15, 16sylc 62 . . . 4 (𝜑𝑧𝑋)
18 tfr1onlemsucaccv.gfn . . . 4 (𝜑𝑔 Fn 𝑧)
19 tfr1onlemsucaccv.gacc . . . 4 (𝜑𝑔𝐴)
2010, 11, 12, 13, 14, 17, 18, 19tfr1onlemsucfn 6338 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn suc 𝑧)
21 vex 2740 . . . . . 6 𝑢 ∈ V
2221elsuc 4405 . . . . 5 (𝑢 ∈ suc 𝑧 ↔ (𝑢𝑧𝑢 = 𝑧))
23 vex 2740 . . . . . . . . . . 11 𝑔 ∈ V
2414tfr1onlem3ag 6335 . . . . . . . . . . 11 (𝑔 ∈ V → (𝑔𝐴 ↔ ∃𝑣𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
2523, 24ax-mp 5 . . . . . . . . . 10 (𝑔𝐴 ↔ ∃𝑣𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
2619, 25sylib 122 . . . . . . . . 9 (𝜑 → ∃𝑣𝑋 (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
27 simprrr 540 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))
28 simprrl 539 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → 𝑔 Fn 𝑣)
2918adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → 𝑔 Fn 𝑧)
30 fndmu 5316 . . . . . . . . . . . 12 ((𝑔 Fn 𝑣𝑔 Fn 𝑧) → 𝑣 = 𝑧)
3128, 29, 30syl2anc 411 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → 𝑣 = 𝑧)
3231raleqdv 2678 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → (∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
3327, 32mpbid 147 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))
3426, 33rexlimddv 2599 . . . . . . . 8 (𝜑 → ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))
3534r19.21bi 2565 . . . . . . 7 ((𝜑𝑢𝑧) → (𝑔𝑢) = (𝐺‘(𝑔𝑢)))
36 ordelon 4382 . . . . . . . . . . . . 13 ((Ord 𝑋𝑧𝑋) → 𝑧 ∈ On)
3712, 17, 36syl2anc 411 . . . . . . . . . . . 12 (𝜑𝑧 ∈ On)
38 onelon 4383 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑢𝑧) → 𝑢 ∈ On)
3937, 38sylan 283 . . . . . . . . . . 11 ((𝜑𝑢𝑧) → 𝑢 ∈ On)
40 eloni 4374 . . . . . . . . . . 11 (𝑢 ∈ On → Ord 𝑢)
41 ordirr 4540 . . . . . . . . . . 11 (Ord 𝑢 → ¬ 𝑢𝑢)
4239, 40, 413syl 17 . . . . . . . . . 10 ((𝜑𝑢𝑧) → ¬ 𝑢𝑢)
43 elequ2 2153 . . . . . . . . . . . 12 (𝑧 = 𝑢 → (𝑢𝑧𝑢𝑢))
4443biimpcd 159 . . . . . . . . . . 11 (𝑢𝑧 → (𝑧 = 𝑢𝑢𝑢))
4544adantl 277 . . . . . . . . . 10 ((𝜑𝑢𝑧) → (𝑧 = 𝑢𝑢𝑢))
4642, 45mtod 663 . . . . . . . . 9 ((𝜑𝑢𝑧) → ¬ 𝑧 = 𝑢)
4746neqned 2354 . . . . . . . 8 ((𝜑𝑢𝑧) → 𝑧𝑢)
48 fvunsng 5709 . . . . . . . 8 ((𝑢 ∈ V ∧ 𝑧𝑢) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝑔𝑢))
4921, 47, 48sylancr 414 . . . . . . 7 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝑔𝑢))
50 eloni 4374 . . . . . . . . . . . 12 (𝑧 ∈ On → Ord 𝑧)
5137, 50syl 14 . . . . . . . . . . 11 (𝜑 → Ord 𝑧)
52 ordelss 4378 . . . . . . . . . . 11 ((Ord 𝑧𝑢𝑧) → 𝑢𝑧)
5351, 52sylan 283 . . . . . . . . . 10 ((𝜑𝑢𝑧) → 𝑢𝑧)
54 resabs1 4935 . . . . . . . . . 10 (𝑢𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))
5553, 54syl 14 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))
56 ordirr 4540 . . . . . . . . . . . . 13 (Ord 𝑧 → ¬ 𝑧𝑧)
5751, 56syl 14 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧𝑧)
58 fsnunres 5717 . . . . . . . . . . . 12 ((𝑔 Fn 𝑧 ∧ ¬ 𝑧𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
5918, 57, 58syl2anc 411 . . . . . . . . . . 11 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
6059reseq1d 4905 . . . . . . . . . 10 (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
6160adantr 276 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
6255, 61eqtr3d 2212 . . . . . . . 8 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢) = (𝑔𝑢))
6362fveq2d 5518 . . . . . . 7 ((𝜑𝑢𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)) = (𝐺‘(𝑔𝑢)))
6435, 49, 633eqtr4d 2220 . . . . . 6 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
65 fneq2 5304 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑓 Fn 𝑥𝑓 Fn 𝑧))
6665imbi1d 231 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ (𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V)))
6766albidv 1824 . . . . . . . . . . 11 (𝑥 = 𝑧 → (∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V)))
68133expia 1205 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → (𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
6968alrimiv 1874 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
7069ralrimiva 2550 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑋𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
7167, 70, 17rspcdva 2846 . . . . . . . . . 10 (𝜑 → ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V))
72 fneq1 5303 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓 Fn 𝑧𝑔 Fn 𝑧))
73 fveq2 5514 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝐺𝑓) = (𝐺𝑔))
7473eleq1d 2246 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝐺𝑓) ∈ V ↔ (𝐺𝑔) ∈ V))
7572, 74imbi12d 234 . . . . . . . . . . 11 (𝑓 = 𝑔 → ((𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V) ↔ (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V)))
7675spv 1860 . . . . . . . . . 10 (∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V) → (𝑔 Fn 𝑧 → (𝐺𝑔) ∈ V))
7771, 18, 76sylc 62 . . . . . . . . 9 (𝜑 → (𝐺𝑔) ∈ V)
78 fndm 5314 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
7918, 78syl 14 . . . . . . . . . 10 (𝜑 → dom 𝑔 = 𝑧)
8057, 79neleqtrrd 2276 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
81 fsnunfv 5716 . . . . . . . . 9 ((𝑧𝑌 ∧ (𝐺𝑔) ∈ V ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
825, 77, 80, 81syl3anc 1238 . . . . . . . 8 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
8382adantr 276 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
84 simpr 110 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → 𝑢 = 𝑧)
8584fveq2d 5518 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧))
86 reseq2 4901 . . . . . . . . 9 (𝑢 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧))
8786, 59sylan9eqr 2232 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢) = 𝑔)
8887fveq2d 5518 . . . . . . 7 ((𝜑𝑢 = 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)) = (𝐺𝑔))
8983, 85, 883eqtr4d 2220 . . . . . 6 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
9064, 89jaodan 797 . . . . 5 ((𝜑 ∧ (𝑢𝑧𝑢 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
9122, 90sylan2b 287 . . . 4 ((𝜑𝑢 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
9291ralrimiva 2550 . . 3 (𝜑 → ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
93 fneq2 5304 . . . . 5 (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn suc 𝑧))
94 raleq 2672 . . . . 5 (𝑤 = suc 𝑧 → (∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)) ↔ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))))
9593, 94anbi12d 473 . . . 4 (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))))
9695rspcev 2841 . . 3 ((suc 𝑧𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))) → ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))))
979, 20, 92, 96syl12anc 1236 . 2 (𝜑 → ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))))
98 vex 2740 . . . . . 6 𝑧 ∈ V
99 opexg 4227 . . . . . 6 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
10098, 77, 99sylancr 414 . . . . 5 (𝜑 → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
101 snexg 4183 . . . . 5 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
102100, 101syl 14 . . . 4 (𝜑 → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
103 unexg 4442 . . . 4 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
10423, 102, 103sylancr 414 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
10514tfr1onlem3ag 6335 . . 3 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))))
106104, 105syl 14 . 2 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴 ↔ ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))))
10797, 106mpbird 167 1 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ 𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  w3a 978  wal 1351   = wceq 1353  wcel 2148  {cab 2163  wne 2347  wral 2455  wrex 2456  Vcvv 2737  cun 3127  wss 3129  {csn 3592  cop 3595   cuni 3809  Ord word 4361  Oncon0 4362  suc csuc 4364  dom cdm 4625  cres 4627  Fun wfun 5209   Fn wfn 5210  cfv 5215  recscrecs 6302
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 4120  ax-pow 4173  ax-pr 4208  ax-un 4432  ax-setind 4535
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 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4003  df-opab 4064  df-tr 4101  df-id 4292  df-iord 4365  df-on 4367  df-suc 4370  df-xp 4631  df-rel 4632  df-cnv 4633  df-co 4634  df-dm 4635  df-res 4637  df-iota 5177  df-fun 5217  df-fn 5218  df-fv 5223
This theorem is referenced by:  tfr1onlembacc  6340  tfr1onlemres  6347
  Copyright terms: Public domain W3C validator