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

Theorem tfr1onlemaccex 6211
 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 4273 . . 3 ((Ord 𝑋𝐶𝑋) → 𝐶 ∈ On)
31, 2sylan 279 . 2 ((𝜑𝐶𝑋) → 𝐶 ∈ On)
4 eleq1 2178 . . . . 5 (𝑧 = 𝑤 → (𝑧𝑋𝑤𝑋))
54anbi2d 457 . . . 4 (𝑧 = 𝑤 → ((𝜑𝑧𝑋) ↔ (𝜑𝑤𝑋)))
6 fneq2 5180 . . . . . 6 (𝑧 = 𝑤 → (𝑔 Fn 𝑧𝑔 Fn 𝑤))
7 raleq 2601 . . . . . 6 (𝑧 = 𝑤 → (∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
86, 7anbi12d 462 . . . . 5 (𝑧 = 𝑤 → ((𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
98exbidv 1779 . . . 4 (𝑧 = 𝑤 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
105, 9imbi12d 233 . . 3 (𝑧 = 𝑤 → (((𝜑𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ ((𝜑𝑤𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
11 eleq1 2178 . . . . 5 (𝑧 = 𝐶 → (𝑧𝑋𝐶𝑋))
1211anbi2d 457 . . . 4 (𝑧 = 𝐶 → ((𝜑𝑧𝑋) ↔ (𝜑𝐶𝑋)))
13 fneq2 5180 . . . . . 6 (𝑧 = 𝐶 → (𝑔 Fn 𝑧𝑔 Fn 𝐶))
14 raleq 2601 . . . . . 6 (𝑧 = 𝐶 → (∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
1513, 14anbi12d 462 . . . . 5 (𝑧 = 𝐶 → ((𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
1615exbidv 1779 . . . 4 (𝑧 = 𝐶 → (∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
1712, 16imbi12d 233 . . 3 (𝑧 = 𝐶 → (((𝜑𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ ((𝜑𝐶𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
18 tfr1on.f . . . . . . . . 9 𝐹 = recs(𝐺)
19 tfr1on.g . . . . . . . . . 10 (𝜑 → Fun 𝐺)
2019ad3antrrr 481 . . . . . . . . 9 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → Fun 𝐺)
211ad3antrrr 481 . . . . . . . . 9 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → Ord 𝑋)
22 tfr1on.ex . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑋𝑓 Fn 𝑥) → (𝐺𝑓) ∈ V)
23223expia 1166 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → (𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
2423alrimiv 1828 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → ∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V))
25 fneq1 5179 . . . . . . . . . . . . . . . . 17 (𝑓 = → (𝑓 Fn 𝑥 Fn 𝑥))
26 fveq2 5387 . . . . . . . . . . . . . . . . . 18 (𝑓 = → (𝐺𝑓) = (𝐺))
2726eleq1d 2184 . . . . . . . . . . . . . . . . 17 (𝑓 = → ((𝐺𝑓) ∈ V ↔ (𝐺) ∈ V))
2825, 27imbi12d 233 . . . . . . . . . . . . . . . 16 (𝑓 = → ((𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ ( Fn 𝑥 → (𝐺) ∈ V)))
2928cbvalv 1869 . . . . . . . . . . . . . . 15 (∀𝑓(𝑓 Fn 𝑥 → (𝐺𝑓) ∈ V) ↔ ∀( Fn 𝑥 → (𝐺) ∈ V))
3024, 29sylib 121 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → ∀( Fn 𝑥 → (𝐺) ∈ V))
313019.21bi 1520 . . . . . . . . . . . . 13 ((𝜑𝑥𝑋) → ( Fn 𝑥 → (𝐺) ∈ V))
32313impia 1161 . . . . . . . . . . . 12 ((𝜑𝑥𝑋 Fn 𝑥) → (𝐺) ∈ V)
33323adant1r 1192 . . . . . . . . . . 11 (((𝜑𝑧 ∈ On) ∧ 𝑥𝑋 Fn 𝑥) → (𝐺) ∈ V)
34333adant1r 1192 . . . . . . . . . 10 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑥𝑋 Fn 𝑥) → (𝐺) ∈ V)
35343adant1r 1192 . . . . . . . . 9 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑥𝑋 Fn 𝑥) → (𝐺) ∈ V)
36 tfr1onlemsucfn.1 . . . . . . . . . 10 𝐴 = {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))}
37 fveq1 5386 . . . . . . . . . . . . . . 15 (𝑓 = → (𝑓𝑦) = (𝑦))
38 reseq1 4781 . . . . . . . . . . . . . . . 16 (𝑓 = → (𝑓𝑦) = (𝑦))
3938fveq2d 5391 . . . . . . . . . . . . . . 15 (𝑓 = → (𝐺‘(𝑓𝑦)) = (𝐺‘(𝑦)))
4037, 39eqeq12d 2130 . . . . . . . . . . . . . 14 (𝑓 = → ((𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ (𝑦) = (𝐺‘(𝑦))))
4140ralbidv 2412 . . . . . . . . . . . . 13 (𝑓 = → (∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)) ↔ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦))))
4225, 41anbi12d 462 . . . . . . . . . . . 12 (𝑓 = → ((𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ( Fn 𝑥 ∧ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦)))))
4342rexbidv 2413 . . . . . . . . . . 11 (𝑓 = → (∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦))) ↔ ∃𝑥𝑋 ( Fn 𝑥 ∧ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦)))))
4443cbvabv 2239 . . . . . . . . . 10 {𝑓 ∣ ∃𝑥𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓𝑦)))} = { ∣ ∃𝑥𝑋 ( Fn 𝑥 ∧ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦)))}
4536, 44eqtri 2136 . . . . . . . . 9 𝐴 = { ∣ ∃𝑥𝑋 ( Fn 𝑥 ∧ ∀𝑦𝑥 (𝑦) = (𝐺‘(𝑦)))}
46 fneq1 5179 . . . . . . . . . . . . . . 15 (𝑟 = 𝑎 → (𝑟 Fn 𝑡𝑎 Fn 𝑡))
47 eleq1 2178 . . . . . . . . . . . . . . 15 (𝑟 = 𝑎 → (𝑟𝐴𝑎𝐴))
48 id 19 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑎𝑟 = 𝑎)
49 fveq2 5387 . . . . . . . . . . . . . . . . . . 19 (𝑟 = 𝑎 → (𝐺𝑟) = (𝐺𝑎))
5049opeq2d 3680 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑎 → ⟨𝑡, (𝐺𝑟)⟩ = ⟨𝑡, (𝐺𝑎)⟩)
5150sneqd 3508 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑎 → {⟨𝑡, (𝐺𝑟)⟩} = {⟨𝑡, (𝐺𝑎)⟩})
5248, 51uneq12d 3199 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑎 → (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩}) = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩}))
5352eqeq2d 2127 . . . . . . . . . . . . . . 15 (𝑟 = 𝑎 → (𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})))
5446, 47, 533anbi123d 1273 . . . . . . . . . . . . . 14 (𝑟 = 𝑎 → ((𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩})) ↔ (𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩}))))
5554cbvexv 1870 . . . . . . . . . . . . 13 (∃𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})))
5655rexbii 2417 . . . . . . . . . . . 12 (∃𝑡𝑧𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩})) ↔ ∃𝑡𝑧𝑎(𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})))
57 fneq2 5180 . . . . . . . . . . . . . . 15 (𝑡 = 𝑏 → (𝑎 Fn 𝑡𝑎 Fn 𝑏))
58 opeq1 3673 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → ⟨𝑡, (𝐺𝑎)⟩ = ⟨𝑏, (𝐺𝑎)⟩)
5958sneqd 3508 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑏 → {⟨𝑡, (𝐺𝑎)⟩} = {⟨𝑏, (𝐺𝑎)⟩})
6059uneq2d 3198 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑏 → (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩}) = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))
6160eqeq2d 2127 . . . . . . . . . . . . . . 15 (𝑡 = 𝑏 → (𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩}) ↔ 𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})))
6257, 613anbi13d 1275 . . . . . . . . . . . . . 14 (𝑡 = 𝑏 → ((𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})) ↔ (𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
6362exbidv 1779 . . . . . . . . . . . . 13 (𝑡 = 𝑏 → (∃𝑎(𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
6463cbvrexv 2630 . . . . . . . . . . . 12 (∃𝑡𝑧𝑎(𝑎 Fn 𝑡𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑡, (𝐺𝑎)⟩})) ↔ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})))
6556, 64bitri 183 . . . . . . . . . . 11 (∃𝑡𝑧𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩})) ↔ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})))
6665abbii 2231 . . . . . . . . . 10 {𝑠 ∣ ∃𝑡𝑧𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩}))} = {𝑠 ∣ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))}
67 eqeq1 2122 . . . . . . . . . . . . . 14 (𝑠 = 𝑑 → (𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}) ↔ 𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})))
68673anbi3d 1279 . . . . . . . . . . . . 13 (𝑠 = 𝑑 → ((𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})) ↔ (𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
6968exbidv 1779 . . . . . . . . . . . 12 (𝑠 = 𝑑 → (∃𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})) ↔ ∃𝑎(𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
7069rexbidv 2413 . . . . . . . . . . 11 (𝑠 = 𝑑 → (∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩})) ↔ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))))
7170cbvabv 2239 . . . . . . . . . 10 {𝑠 ∣ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑠 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))} = {𝑑 ∣ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))}
7266, 71eqtri 2136 . . . . . . . . 9 {𝑠 ∣ ∃𝑡𝑧𝑟(𝑟 Fn 𝑡𝑟𝐴𝑠 = (𝑟 ∪ {⟨𝑡, (𝐺𝑟)⟩}))} = {𝑑 ∣ ∃𝑏𝑧𝑎(𝑎 Fn 𝑏𝑎𝐴𝑑 = (𝑎 ∪ {⟨𝑏, (𝐺𝑎)⟩}))}
73 tfr1onlemaccex.u . . . . . . . . . . . 12 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
7473adantlr 466 . . . . . . . . . . 11 (((𝜑𝑧 ∈ On) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
7574adantlr 466 . . . . . . . . . 10 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
7675adantlr 466 . . . . . . . . 9 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
77 simpr 109 . . . . . . . . 9 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → 𝑧𝑋)
78 simpr 109 . . . . . . . . . . . 12 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → 𝑏𝑧)
79 simplr 502 . . . . . . . . . . . 12 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → 𝑧𝑋)
80 ordtr1 4278 . . . . . . . . . . . . . 14 (Ord 𝑋 → ((𝑏𝑧𝑧𝑋) → 𝑏𝑋))
811, 80syl 14 . . . . . . . . . . . . 13 (𝜑 → ((𝑏𝑧𝑧𝑋) → 𝑏𝑋))
8281ad4antr 483 . . . . . . . . . . . 12 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → ((𝑏𝑧𝑧𝑋) → 𝑏𝑋))
8378, 79, 82mp2and 427 . . . . . . . . . . 11 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → 𝑏𝑋)
84 eleq1 2178 . . . . . . . . . . . . . 14 (𝑤 = 𝑏 → (𝑤𝑋𝑏𝑋))
85 fneq2 5180 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑏 → (𝑔 Fn 𝑤𝑔 Fn 𝑏))
86 raleq 2601 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑏 → (∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
8785, 86anbi12d 462 . . . . . . . . . . . . . . 15 (𝑤 = 𝑏 → ((𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
8887exbidv 1779 . . . . . . . . . . . . . 14 (𝑤 = 𝑏 → (∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
8984, 88imbi12d 233 . . . . . . . . . . . . 13 (𝑤 = 𝑏 → ((𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ (𝑏𝑋 → ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
90 simpllr 506 . . . . . . . . . . . . 13 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
9189, 90, 78rspcdva 2766 . . . . . . . . . . . 12 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → (𝑏𝑋 → ∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
92 fneq1 5179 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (𝑔 Fn 𝑏𝑎 Fn 𝑏))
93 fveq1 5386 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑎 → (𝑔𝑢) = (𝑎𝑢))
94 reseq1 4781 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑎 → (𝑔𝑢) = (𝑎𝑢))
9594fveq2d 5391 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑎 → (𝐺‘(𝑔𝑢)) = (𝐺‘(𝑎𝑢)))
9693, 95eqeq12d 2130 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑎 → ((𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ (𝑎𝑢) = (𝐺‘(𝑎𝑢))))
9796ralbidv 2412 . . . . . . . . . . . . . . 15 (𝑔 = 𝑎 → (∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢)) ↔ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢))))
9892, 97anbi12d 462 . . . . . . . . . . . . . 14 (𝑔 = 𝑎 → ((𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢)))))
9998cbvexv 1870 . . . . . . . . . . . . 13 (∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢))))
100 fveq2 5387 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑐 → (𝑎𝑢) = (𝑎𝑐))
101 reseq2 4782 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑐 → (𝑎𝑢) = (𝑎𝑐))
102101fveq2d 5391 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑐 → (𝐺‘(𝑎𝑢)) = (𝐺‘(𝑎𝑐)))
103100, 102eqeq12d 2130 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑐 → ((𝑎𝑢) = (𝐺‘(𝑎𝑢)) ↔ (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
104103cbvralv 2629 . . . . . . . . . . . . . . 15 (∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢)) ↔ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐)))
105104anbi2i 450 . . . . . . . . . . . . . 14 ((𝑎 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢))) ↔ (𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
106105exbii 1567 . . . . . . . . . . . . 13 (∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑎𝑢) = (𝐺‘(𝑎𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
10799, 106bitri 183 . . . . . . . . . . . 12 (∃𝑔(𝑔 Fn 𝑏 ∧ ∀𝑢𝑏 (𝑔𝑢) = (𝐺‘(𝑔𝑢))) ↔ ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
10891, 107syl6ib 160 . . . . . . . . . . 11 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → (𝑏𝑋 → ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐)))))
10983, 108mpd 13 . . . . . . . . . 10 (((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) ∧ 𝑏𝑧) → ∃𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
110109ralrimiva 2480 . . . . . . . . 9 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → ∀𝑏𝑧𝑎(𝑎 Fn 𝑏 ∧ ∀𝑐𝑏 (𝑎𝑐) = (𝐺‘(𝑎𝑐))))
11118, 20, 21, 35, 45, 72, 76, 77, 110tfr1onlemex 6210 . . . . . . . 8 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → ∃( Fn 𝑧 ∧ ∀𝑢𝑧 (𝑢) = (𝐺‘(𝑢))))
112 fneq1 5179 . . . . . . . . . 10 ( = 𝑔 → ( Fn 𝑧𝑔 Fn 𝑧))
113 fveq1 5386 . . . . . . . . . . . 12 ( = 𝑔 → (𝑢) = (𝑔𝑢))
114 reseq1 4781 . . . . . . . . . . . . 13 ( = 𝑔 → (𝑢) = (𝑔𝑢))
115114fveq2d 5391 . . . . . . . . . . . 12 ( = 𝑔 → (𝐺‘(𝑢)) = (𝐺‘(𝑔𝑢)))
116113, 115eqeq12d 2130 . . . . . . . . . . 11 ( = 𝑔 → ((𝑢) = (𝐺‘(𝑢)) ↔ (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
117116ralbidv 2412 . . . . . . . . . 10 ( = 𝑔 → (∀𝑢𝑧 (𝑢) = (𝐺‘(𝑢)) ↔ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
118112, 117anbi12d 462 . . . . . . . . 9 ( = 𝑔 → (( Fn 𝑧 ∧ ∀𝑢𝑧 (𝑢) = (𝐺‘(𝑢))) ↔ (𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
119118cbvexv 1870 . . . . . . . 8 (∃( Fn 𝑧 ∧ ∀𝑢𝑧 (𝑢) = (𝐺‘(𝑢))) ↔ ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
120111, 119sylib 121 . . . . . . 7 ((((𝜑𝑧 ∈ On) ∧ ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) ∧ 𝑧𝑋) → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
121120exp31 359 . . . . . 6 ((𝜑𝑧 ∈ On) → (∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (𝑧𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
122121expcom 115 . . . . 5 (𝑧 ∈ On → (𝜑 → (∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) → (𝑧𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))))
123122a2d 26 . . . 4 (𝑧 ∈ On → ((𝜑 → ∀𝑤𝑧 (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))) → (𝜑 → (𝑧𝑋 → ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑢𝑧 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))))
124 impexp 261 . . . . . 6 (((𝜑𝑤𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ (𝜑 → (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
125124ralbii 2416 . . . . 5 (∀𝑤𝑧 ((𝜑𝑤𝑋) → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))) ↔ ∀𝑤𝑧 (𝜑 → (𝑤𝑋 → ∃𝑔(𝑔 Fn 𝑤 ∧ ∀𝑢𝑤 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))))
126 r19.21v 2484 . . . . 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 4468 . 2 (𝐶 ∈ On → ((𝜑𝐶𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢)))))
1313, 130mpcom 36 1 ((𝜑𝐶𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢𝐶 (𝑔𝑢) = (𝐺‘(𝑔𝑢))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 945  ∀wal 1312   = wceq 1314  ∃wex 1451   ∈ wcel 1463  {cab 2101  ∀wral 2391  ∃wrex 2392  Vcvv 2658   ∪ cun 3037  {csn 3495  ⟨cop 3498  ∪ cuni 3704  Ord word 4252  Oncon0 4253  suc csuc 4255   ↾ cres 4509  Fun wfun 5085   Fn wfn 5086  ‘cfv 5091  recscrecs 6167 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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420 This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-reu 2398  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-iord 4256  df-on 4258  df-suc 4261  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-recs 6168 This theorem is referenced by:  tfr1onlemres  6212
 Copyright terms: Public domain W3C validator