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

Theorem tfr1onlemsucaccv 6344
Description: Lemma for tfr1on 6353. 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 4404 . . . . 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 3816 . . . . 5 ((𝑧𝑌𝑌𝑋) → 𝑧 𝑋)
85, 6, 7syl2anc 411 . . . 4 (𝜑𝑧 𝑋)
92, 4, 8rspcdva 2848 . . 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 4390 . . . . 5 (Ord 𝑋 → ((𝑧𝑌𝑌𝑋) → 𝑧𝑋))
1712, 15, 16sylc 62 . . . 4 (𝜑𝑧𝑋)
18 tfr1onlemsucaccv.gfn . . . 4 (𝜑𝑔 Fn 𝑧)
19 tfr1onlemsucaccv.gacc . . . 4 (𝜑𝑔𝐴)
2010, 11, 12, 13, 14, 17, 18, 19tfr1onlemsucfn 6343 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn suc 𝑧)
21 vex 2742 . . . . . 6 𝑢 ∈ V
2221elsuc 4408 . . . . 5 (𝑢 ∈ suc 𝑧 ↔ (𝑢𝑧𝑢 = 𝑧))
23 vex 2742 . . . . . . . . . . 11 𝑔 ∈ V
2414tfr1onlem3ag 6340 . . . . . . . . . . 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 5319 . . . . . . . . . . . 12 ((𝑔 Fn 𝑣𝑔 Fn 𝑧) → 𝑣 = 𝑧)
3128, 29, 30syl2anc 411 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → 𝑣 = 𝑧)
3231raleqdv 2679 . . . . . . . . . 10 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → (∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
3327, 32mpbid 147 . . . . . . . . 9 ((𝜑 ∧ (𝑣𝑋 ∧ (𝑔 Fn 𝑣 ∧ ∀𝑢𝑣 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))
3426, 33rexlimddv 2599 . . . . . . . 8 (𝜑 → ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))
3534r19.21bi 2565 . . . . . . 7 ((𝜑𝑢𝑧) → (𝑔𝑢) = (𝐺‘(𝑔𝑢)))
36 ordelon 4385 . . . . . . . . . . . . 13 ((Ord 𝑋𝑧𝑋) → 𝑧 ∈ On)
3712, 17, 36syl2anc 411 . . . . . . . . . . . 12 (𝜑𝑧 ∈ On)
38 onelon 4386 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑢𝑧) → 𝑢 ∈ On)
3937, 38sylan 283 . . . . . . . . . . 11 ((𝜑𝑢𝑧) → 𝑢 ∈ On)
40 eloni 4377 . . . . . . . . . . 11 (𝑢 ∈ On → Ord 𝑢)
41 ordirr 4543 . . . . . . . . . . 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 5712 . . . . . . . 8 ((𝑢 ∈ V ∧ 𝑧𝑢) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝑔𝑢))
4921, 47, 48sylancr 414 . . . . . . 7 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝑔𝑢))
50 eloni 4377 . . . . . . . . . . . 12 (𝑧 ∈ On → Ord 𝑧)
5137, 50syl 14 . . . . . . . . . . 11 (𝜑 → Ord 𝑧)
52 ordelss 4381 . . . . . . . . . . 11 ((Ord 𝑧𝑢𝑧) → 𝑢𝑧)
5351, 52sylan 283 . . . . . . . . . 10 ((𝜑𝑢𝑧) → 𝑢𝑧)
54 resabs1 4938 . . . . . . . . . 10 (𝑢𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))
5553, 54syl 14 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))
56 ordirr 4543 . . . . . . . . . . . . 13 (Ord 𝑧 → ¬ 𝑧𝑧)
5751, 56syl 14 . . . . . . . . . . . 12 (𝜑 → ¬ 𝑧𝑧)
58 fsnunres 5720 . . . . . . . . . . . 12 ((𝑔 Fn 𝑧 ∧ ¬ 𝑧𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
5918, 57, 58syl2anc 411 . . . . . . . . . . 11 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) = 𝑔)
6059reseq1d 4908 . . . . . . . . . 10 (𝜑 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
6160adantr 276 . . . . . . . . 9 ((𝜑𝑢𝑧) → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧) ↾ 𝑢) = (𝑔𝑢))
6255, 61eqtr3d 2212 . . . . . . . 8 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢) = (𝑔𝑢))
6362fveq2d 5521 . . . . . . 7 ((𝜑𝑢𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)) = (𝐺‘(𝑔𝑢)))
6435, 49, 633eqtr4d 2220 . . . . . 6 ((𝜑𝑢𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
65 fneq2 5307 . . . . . . . . . . . . 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 2848 . . . . . . . . . 10 (𝜑 → ∀𝑓(𝑓 Fn 𝑧 → (𝐺𝑓) ∈ V))
72 fneq1 5306 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑓 Fn 𝑧𝑔 Fn 𝑧))
73 fveq2 5517 . . . . . . . . . . . . 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 5317 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
7918, 78syl 14 . . . . . . . . . 10 (𝜑 → dom 𝑔 = 𝑧)
8057, 79neleqtrrd 2276 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝑔)
81 fsnunfv 5719 . . . . . . . . 9 ((𝑧𝑌 ∧ (𝐺𝑔) ∈ V ∧ ¬ 𝑧 ∈ dom 𝑔) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
825, 77, 80, 81syl3anc 1238 . . . . . . . 8 (𝜑 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
8382adantr 276 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧) = (𝐺𝑔))
84 simpr 110 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → 𝑢 = 𝑧)
8584fveq2d 5521 . . . . . . 7 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑧))
86 reseq2 4904 . . . . . . . . 9 (𝑢 = 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢) = ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑧))
8786, 59sylan9eqr 2232 . . . . . . . 8 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢) = 𝑔)
8887fveq2d 5521 . . . . . . 7 ((𝜑𝑢 = 𝑧) → (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)) = (𝐺𝑔))
8983, 85, 883eqtr4d 2220 . . . . . 6 ((𝜑𝑢 = 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
9064, 89jaodan 797 . . . . 5 ((𝜑 ∧ (𝑢𝑧𝑢 = 𝑧)) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
9122, 90sylan2b 287 . . . 4 ((𝜑𝑢 ∈ suc 𝑧) → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
9291ralrimiva 2550 . . 3 (𝜑 → ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))
93 fneq2 5307 . . . . 5 (𝑤 = suc 𝑧 → ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ↔ (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn suc 𝑧))
94 raleq 2673 . . . . 5 (𝑤 = suc 𝑧 → (∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)) ↔ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))))
9593, 94anbi12d 473 . . . 4 (𝑤 = suc 𝑧 → (((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))) ↔ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))))
9695rspcev 2843 . . 3 ((suc 𝑧𝑋 ∧ ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn suc 𝑧 ∧ ∀𝑢 ∈ suc 𝑧((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢)))) → ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))))
979, 20, 92, 96syl12anc 1236 . 2 (𝜑 → ∃𝑤𝑋 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) Fn 𝑤 ∧ ∀𝑢𝑤 ((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩})‘𝑢) = (𝐺‘((𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ↾ 𝑢))))
98 vex 2742 . . . . . 6 𝑧 ∈ V
99 opexg 4230 . . . . . 6 ((𝑧 ∈ V ∧ (𝐺𝑔) ∈ V) → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
10098, 77, 99sylancr 414 . . . . 5 (𝜑 → ⟨𝑧, (𝐺𝑔)⟩ ∈ V)
101 snexg 4186 . . . . 5 (⟨𝑧, (𝐺𝑔)⟩ ∈ V → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
102100, 101syl 14 . . . 4 (𝜑 → {⟨𝑧, (𝐺𝑔)⟩} ∈ V)
103 unexg 4445 . . . 4 ((𝑔 ∈ V ∧ {⟨𝑧, (𝐺𝑔)⟩} ∈ V) → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
10423, 102, 103sylancr 414 . . 3 (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐺𝑔)⟩}) ∈ V)
10514tfr1onlem3ag 6340 . . 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 2739  cun 3129  wss 3131  {csn 3594  cop 3597   cuni 3811  Ord word 4364  Oncon0 4365  suc csuc 4367  dom cdm 4628  cres 4630  Fun wfun 5212   Fn wfn 5213  cfv 5218  recscrecs 6307
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 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538
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 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-tr 4104  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-res 4640  df-iota 5180  df-fun 5220  df-fn 5221  df-fv 5226
This theorem is referenced by:  tfr1onlembacc  6345  tfr1onlemres  6352
  Copyright terms: Public domain W3C validator