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

Theorem tfr1onlemaccex 6325
Description: We can define an acceptable function on any element of 𝑋.

As with many of the transfinite recursion theorems, we have hypotheses that state that 𝐹 is a function and that it is defined up to 𝑋. (Contributed by Jim Kingdon, 16-Mar-2022.)

Hypotheses
Ref Expression
tfr1on.f 𝐹 = recs(𝐺)
tfr1on.g (𝜑 → Fun 𝐺)
tfr1on.x (𝜑 → Ord 𝑋)
tfr1on.ex ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
tfr1onlemsucfn.1 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
tfr1onlemaccex.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
Assertion
Ref Expression
tfr1onlemaccex ((𝜑𝐶𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
Distinct variable groups:   𝑢,𝐴,𝑥   𝐶,𝑔,𝑢   𝑔,𝐺,𝑢,𝑥   𝑓,𝐺,𝑦,𝑥   𝑥,𝑋,𝑓   𝜑,𝑥   𝑦,𝑔   𝜑,𝑓
Allowed substitution hints:   𝜑(𝑦,𝑢,𝑔)   𝐴(𝑦,𝑓,𝑔)   𝐶(𝑥,𝑦,𝑓)   𝐹(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑋(𝑦,𝑢,𝑔)

Proof of Theorem tfr1onlemaccex
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑟 𝑠 𝑡 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfr1on.x . . 3 (𝜑 → Ord 𝑋)
2 ordelon 4366 . . 3 ((Ord 𝑋𝐶𝑋) → 𝐶 ∈ On)
31, 2sylan 281 . 2 ((𝜑𝐶𝑋) → 𝐶 ∈ On)
4 eleq1 2233 . . . . 5 (𝑧 = 𝑤 → (𝑧𝑋𝑤𝑋))
54anbi2d 461 . . . 4 (𝑧 = 𝑤 → ((𝜑𝑧𝑋) ↔ (𝜑𝑤𝑋)))
6 fneq2 5285 . . . . . 6 (𝑧 = 𝑤 → (𝑔 Fn 𝑧𝑔 Fn 𝑤))
7 raleq 2665 . . . . . 6 (𝑧 = 𝑤 → (∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
86, 7anbi12d 470 . . . . 5 (𝑧 = 𝑤 → ((𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
98exbidv 1818 . . . 4 (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
105, 9imbi12d 233 . . 3 (𝑧 = 𝑤 → (((𝜑𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ ((𝜑𝑤𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
11 eleq1 2233 . . . . 5 (𝑧 = 𝐶 → (𝑧𝑋𝐶𝑋))
1211anbi2d 461 . . . 4 (𝑧 = 𝐶 → ((𝜑𝑧𝑋) ↔ (𝜑𝐶𝑋)))
13 fneq2 5285 . . . . . 6 (𝑧 = 𝐶 → (𝑔 Fn 𝑧𝑔 Fn 𝐶))
14 raleq 2665 . . . . . 6 (𝑧 = 𝐶 → (∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
1513, 14anbi12d 470 . . . . 5 (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
1615exbidv 1818 . . . 4 (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
1712, 16imbi12d 233 . . 3 (𝑧 = 𝐶 → (((𝜑𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ ((𝜑𝐶𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
18 tfr1on.f . . . . . . . . 9 𝐹 = recs(𝐺)
19 tfr1on.g . . . . . . . . . 10 (𝜑 → Fun 𝐺)
2019ad3antrrr 489 . . . . . . . . 9 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → Fun 𝐺)
211ad3antrrr 489 . . . . . . . . 9 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → Ord 𝑋)
22 tfr1on.ex . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
23223expia 1200 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → (𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
2423alrimiv 1867 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
25 fneq1 5284 . . . . . . . . . . . . . . . . 17 (𝑓 = → (𝑓 Fn 𝑥 Fn 𝑥))
26 fveq2 5494 . . . . . . . . . . . . . . . . . 18 (𝑓 = → (𝐺𝑓) = (𝐺))
2726eleq1d 2239 . . . . . . . . . . . . . . . . 17 (𝑓 = → ((𝐺𝑓) ∈ V ↔ (𝐺) ∈ V))
2825, 27imbi12d 233 . . . . . . . . . . . . . . . 16 (𝑓 = → ((𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ ( Fn 𝑥 → (𝐺) ∈ V)))
2928cbvalv 1910 . . . . . . . . . . . . . . 15 (∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ ∀( Fn 𝑥 → (𝐺) ∈ V))
3024, 29sylib 121 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → ∀( Fn 𝑥 → (𝐺) ∈ V))
313019.21bi 1551 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ( Fn 𝑥 → (𝐺) ∈ V))
32313impia 1195 . . . . . . . . . . . 12 ((𝜑𝑥𝑋 Fn 𝑥) → (𝐺) ∈ V)
33323adant1r 1226 . . . . . . . . . . 11 (((𝜑𝑧 ∈ On) ∧ 𝑥𝑋 Fn 𝑥) → (𝐺) ∈ V)
34333adant1r 1226 . . . . . . . . . 10 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑥𝑋 Fn 𝑥) → (𝐺) ∈ V)
35343adant1r 1226 . . . . . . . . 9 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑥𝑋 Fn 𝑥) → (𝐺) ∈ V)
36 tfr1onlemsucfn.1 . . . . . . . . . 10 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
37 fveq1 5493 . . . . . . . . . . . . . . 15 (𝑓 = → (𝑓𝑦) = (𝑦))
38 reseq1 4883 . . . . . . . . . . . . . . . 16 (𝑓 = → (𝑓𝑦) = (𝑦))
3938fveq2d 5498 . . . . . . . . . . . . . . 15 (𝑓 = → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑦)))
4037, 39eqeq12d 2185 . . . . . . . . . . . . . 14 (𝑓 = → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑦) = (𝐺‘(𝑦))))
4140ralbidv 2470 . . . . . . . . . . . . 13 (𝑓 = → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦))))
4225, 41anbi12d 470 . . . . . . . . . . . 12 (𝑓 = → ((𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ( Fn 𝑥 ∧ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦)))))
4342rexbidv 2471 . . . . . . . . . . 11 (𝑓 = → (∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 ( Fn 𝑥 ∧ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦)))))
4443cbvabv 2295 . . . . . . . . . 10 {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} = { ∣ ∃𝑥𝑋 ( Fn 𝑥 ∧ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦)))}
4536, 44eqtri 2191 . . . . . . . . 9 𝐴 = { ∣ ∃𝑥𝑋 ( Fn 𝑥 ∧ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦)))}
46 fneq1 5284 . . . . . . . . . . . . . . 15 (𝑟 = 𝑎 → (𝑟 Fn 𝑡𝑎 Fn 𝑡))
47 eleq1 2233 . . . . . . . . . . . . . . 15 (𝑟 = 𝑎 → (𝑟𝐴𝑎𝐴))
48 id 19 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑎𝑟 = 𝑎)
49 fveq2 5494 . . . . . . . . . . . . . . . . . . 19 (𝑟 = 𝑎 → (𝐺𝑟) = (𝐺𝑎))
5049opeq2d 3770 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑎 → ⟨𝑡, (𝐺𝑟)⟩ = ⟨𝑡, (𝐺𝑎)⟩)
5150sneqd 3594 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑎 → {⟨𝑡, (𝐺𝑟)⟩} = {⟨𝑡, (𝐺𝑎)⟩})
5248, 51uneq12d 3282 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑎 → (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩}) = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩}))
5352eqeq2d 2182 . . . . . . . . . . . . . . 15 (𝑟 = 𝑎 → (𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})))
5446, 47, 533anbi123d 1307 . . . . . . . . . . . . . 14 (𝑟 = 𝑎 → ((𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩})) ↔ (𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩}))))
5554cbvexv 1911 . . . . . . . . . . . . 13 (∃𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})))
5655rexbii 2477 . . . . . . . . . . . 12 (∃𝑡𝑧𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩})) ↔ ∃𝑡𝑧𝑎(𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})))
57 fneq2 5285 . . . . . . . . . . . . . . 15 (𝑡 = 𝑏 → (𝑎 Fn 𝑡𝑎 Fn 𝑏))
58 opeq1 3763 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → ⟨𝑡, (𝐺𝑎)⟩ = ⟨𝑏, (𝐺𝑎)⟩)
5958sneqd 3594 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑏 → {⟨𝑡, (𝐺𝑎)⟩} = {⟨𝑏, (𝐺𝑎)⟩})
6059uneq2d 3281 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑏 → (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩}) = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))
6160eqeq2d 2182 . . . . . . . . . . . . . . 15 (𝑡 = 𝑏 → (𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})))
6257, 613anbi13d 1309 . . . . . . . . . . . . . 14 (𝑡 = 𝑏 → ((𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})) ↔ (𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
6362exbidv 1818 . . . . . . . . . . . . 13 (𝑡 = 𝑏 → (∃𝑎(𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
6463cbvrexv 2697 . . . . . . . . . . . 12 (∃𝑡𝑧𝑎(𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})) ↔ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})))
6556, 64bitri 183 . . . . . . . . . . 11 (∃𝑡𝑧𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩})) ↔ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})))
6665abbii 2286 . . . . . . . . . 10 {𝑠 ∣ ∃𝑡𝑧𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩}))} = {𝑠 ∣ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))}
67 eqeq1 2177 . . . . . . . . . . . . . 14 (𝑠 = 𝑑 → (𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}) ↔ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})))
68673anbi3d 1313 . . . . . . . . . . . . 13 (𝑠 = 𝑑 → ((𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})) ↔ (𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
6968exbidv 1818 . . . . . . . . . . . 12 (𝑠 = 𝑑 → (∃𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
7069rexbidv 2471 . . . . . . . . . . 11 (𝑠 = 𝑑 → (∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})) ↔ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
7170cbvabv 2295 . . . . . . . . . 10 {𝑠 ∣ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))} = {𝑑 ∣ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))}
7266, 71eqtri 2191 . . . . . . . . 9 {𝑠 ∣ ∃𝑡𝑧𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩}))} = {𝑑 ∣ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))}
73 tfr1onlemaccex.u . . . . . . . . . . . 12 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
7473adantlr 474 . . . . . . . . . . 11 (((𝜑𝑧 ∈ On) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
7574adantlr 474 . . . . . . . . . 10 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
7675adantlr 474 . . . . . . . . 9 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
77 simpr 109 . . . . . . . . 9 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → 𝑧𝑋)
78 simpr 109 . . . . . . . . . . . 12 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → 𝑏𝑧)
79 simplr 525 . . . . . . . . . . . 12 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → 𝑧𝑋)
80 ordtr1 4371 . . . . . . . . . . . . . 14 (Ord 𝑋 → ((𝑏𝑧𝑧𝑋) → 𝑏𝑋))
811, 80syl 14 . . . . . . . . . . . . 13 (𝜑 → ((𝑏𝑧𝑧𝑋) → 𝑏𝑋))
8281ad4antr 491 . . . . . . . . . . . 12 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → ((𝑏𝑧𝑧𝑋) → 𝑏𝑋))
8378, 79, 82mp2and 431 . . . . . . . . . . 11 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → 𝑏𝑋)
84 eleq1 2233 . . . . . . . . . . . . . 14 (𝑤 = 𝑏 → (𝑤𝑋𝑏𝑋))
85 fneq2 5285 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑏 → (𝑔 Fn 𝑤𝑔 Fn 𝑏))
86 raleq 2665 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑏 → (∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
8785, 86anbi12d 470 . . . . . . . . . . . . . . 15 (𝑤 = 𝑏 → ((𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
8887exbidv 1818 . . . . . . . . . . . . . 14 (𝑤 = 𝑏 → (∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
8984, 88imbi12d 233 . . . . . . . . . . . . 13 (𝑤 = 𝑏 → ((𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ (𝑏𝑋 → ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
90 simpllr 529 . . . . . . . . . . . . 13 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
9189, 90, 78rspcdva 2839 . . . . . . . . . . . 12 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → (𝑏𝑋 → ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
92 fneq1 5284 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (𝑔 Fn 𝑏𝑎 Fn 𝑏))
93 fveq1 5493 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑎 → (𝑔𝑢) = (𝑎𝑢))
94 reseq1 4883 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑎 → (𝑔𝑢) = (𝑎𝑢))
9594fveq2d 5498 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑎 → (𝐺‘(𝑔𝑢)) = (𝐺‘(𝑎𝑢)))
9693, 95eqeq12d 2185 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑎 → ((𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ (𝑎𝑢) = (𝐺‘(𝑎𝑢))))
9796ralbidv 2470 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢))))
9892, 97anbi12d 470 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → ((𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢)))))
9998cbvexv 1911 . . . . . . . . . . . . 13 (∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢))))
100 fveq2 5494 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑐 → (𝑎𝑢) = (𝑎𝑐))
101 reseq2 4884 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑐 → (𝑎𝑢) = (𝑎𝑐))
102101fveq2d 5498 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑐 → (𝐺‘(𝑎𝑢)) = (𝐺‘(𝑎𝑐)))
103100, 102eqeq12d 2185 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑐 → ((𝑎𝑢) = (𝐺‘(𝑎𝑢)) ↔ (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
104103cbvralv 2696 . . . . . . . . . . . . . . 15 (∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢)) ↔ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐)))
105104anbi2i 454 . . . . . . . . . . . . . 14 ((𝑎 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
106105exbii 1598 . . . . . . . . . . . . 13 (∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
10799, 106bitri 183 . . . . . . . . . . . 12 (∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
10891, 107syl6ib 160 . . . . . . . . . . 11 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → (𝑏𝑋 → ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐)))))
10983, 108mpd 13 . . . . . . . . . 10 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
110109ralrimiva 2543 . . . . . . . . 9 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → ∀𝑏𝑧𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
11118, 20, 21, 35, 45, 72, 76, 77, 110tfr1onlemex 6324 . . . . . . . 8 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → ∃( Fn 𝑧 ∧ ∀𝑢𝑧 (𝑢) = (𝐺‘(𝑢))))
112 fneq1 5284 . . . . . . . . . 10 ( = 𝑔 → ( Fn 𝑧𝑔 Fn 𝑧))
113 fveq1 5493 . . . . . . . . . . . 12 ( = 𝑔 → (𝑢) = (𝑔𝑢))
114 reseq1 4883 . . . . . . . . . . . . 13 ( = 𝑔 → (𝑢) = (𝑔𝑢))
115114fveq2d 5498 . . . . . . . . . . . 12 ( = 𝑔 → (𝐺‘(𝑢)) = (𝐺‘(𝑔𝑢)))
116113, 115eqeq12d 2185 . . . . . . . . . . 11 ( = 𝑔 → ((𝑢) = (𝐺‘(𝑢)) ↔ (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
117116ralbidv 2470 . . . . . . . . . 10 ( = 𝑔 → (∀𝑢𝑧 (𝑢) = (𝐺‘(𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
118112, 117anbi12d 470 . . . . . . . . 9 ( = 𝑔 → (( Fn 𝑧 ∧ ∀𝑢𝑧 (𝑢) = (𝐺‘(𝑢))) ↔ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
119118cbvexv 1911 . . . . . . . 8 (∃( Fn 𝑧 ∧ ∀𝑢𝑧 (𝑢) = (𝐺‘(𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
120111, 119sylib 121 . . . . . . 7 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
121120exp31 362 . . . . . 6 ((𝜑𝑧 ∈ On) → (∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (𝑧𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
122121expcom 115 . . . . 5 (𝑧 ∈ On → (𝜑 → (∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (𝑧𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))))
123122a2d 26 . . . 4 (𝑧 ∈ On → ((𝜑 → ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → (𝜑 → (𝑧𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))))
124 impexp 261 . . . . . 6 (((𝜑𝑤𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ (𝜑 → (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
125124ralbii 2476 . . . . 5 (∀𝑤𝑧 ((𝜑𝑤𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ ∀𝑤𝑧 (𝜑 → (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
126 r19.21v 2547 . . . . 5 (∀𝑤𝑧 (𝜑 → (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ↔ (𝜑 → ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
127125, 126bitri 183 . . . 4 (∀𝑤𝑧 ((𝜑𝑤𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ (𝜑 → ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
128 impexp 261 . . . 4 (((𝜑𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ (𝜑 → (𝑧𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
129123, 127, 1283imtr4g 204 . . 3 (𝑧 ∈ On → (∀𝑤𝑧 ((𝜑𝑤𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → ((𝜑𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
13010, 17, 129tfis3 4568 . 2 (𝐶 ∈ On → ((𝜑𝐶𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
1313, 130mpcom 36 1 ((𝜑𝐶𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 973  wal 1346   = wceq 1348  wex 1485  wcel 2141  {cab 2156  wral 2448  wrex 2449  Vcvv 2730  cun 3119  {csn 3581  cop 3584   cuni 3794  Ord word 4345  Oncon0 4346  suc csuc 4348  cres 4611  Fun wfun 5190   Fn wfn 5191  cfv 5196  recscrecs 6281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-iord 4349  df-on 4351  df-suc 4354  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-recs 6282
This theorem is referenced by:  tfr1onlemres  6326
  Copyright terms: Public domain W3C validator