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

Theorem tfrcl 6368
Description: Closure for transfinite recursion. As with tfr1on 6354, the characteristic function must be defined up to a suitable point, not necessarily on all ordinals. (Contributed by Jim Kingdon, 25-Mar-2022.)
Hypotheses
Ref Expression
tfrcl.f 𝐹 = recs(𝐺)
tfrcl.g (𝜑 → Fun 𝐺)
tfrcl.x (𝜑 → Ord 𝑋)
tfrcl.ex ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
tfrcl.u ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
tfrcl.yx (𝜑𝑌 𝑋)
Assertion
Ref Expression
tfrcl (𝜑 → (𝐹𝑌) ∈ 𝑆)
Distinct variable groups:   𝑓,𝐹,𝑥   𝑓,𝐺,𝑥   𝑆,𝑓,𝑥   𝑓,𝑋,𝑥   𝜑,𝑓,𝑥
Allowed substitution hints:   𝑌(𝑥,𝑓)

Proof of Theorem tfrcl
Dummy variables 𝑘 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrcl.x . . . 4 (𝜑 → Ord 𝑋)
2 orduni 4496 . . . 4 (Ord 𝑋 → Ord 𝑋)
31, 2syl 14 . . 3 (𝜑 → Ord 𝑋)
4 tfrcl.yx . . 3 (𝜑𝑌 𝑋)
5 ordelon 4385 . . 3 ((Ord 𝑋𝑌 𝑋) → 𝑌 ∈ On)
63, 4, 5syl2anc 411 . 2 (𝜑𝑌 ∈ On)
74ancli 323 . 2 (𝜑 → (𝜑𝑌 𝑋))
8 eleq1 2240 . . . . 5 (𝑤 = 𝑘 → (𝑤 𝑋𝑘 𝑋))
98anbi2d 464 . . . 4 (𝑤 = 𝑘 → ((𝜑𝑤 𝑋) ↔ (𝜑𝑘 𝑋)))
10 fveq2 5517 . . . . 5 (𝑤 = 𝑘 → (𝐹𝑤) = (𝐹𝑘))
1110eleq1d 2246 . . . 4 (𝑤 = 𝑘 → ((𝐹𝑤) ∈ 𝑆 ↔ (𝐹𝑘) ∈ 𝑆))
129, 11imbi12d 234 . . 3 (𝑤 = 𝑘 → (((𝜑𝑤 𝑋) → (𝐹𝑤) ∈ 𝑆) ↔ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)))
13 eleq1 2240 . . . . 5 (𝑤 = 𝑌 → (𝑤 𝑋𝑌 𝑋))
1413anbi2d 464 . . . 4 (𝑤 = 𝑌 → ((𝜑𝑤 𝑋) ↔ (𝜑𝑌 𝑋)))
15 fveq2 5517 . . . . 5 (𝑤 = 𝑌 → (𝐹𝑤) = (𝐹𝑌))
1615eleq1d 2246 . . . 4 (𝑤 = 𝑌 → ((𝐹𝑤) ∈ 𝑆 ↔ (𝐹𝑌) ∈ 𝑆))
1714, 16imbi12d 234 . . 3 (𝑤 = 𝑌 → (((𝜑𝑤 𝑋) → (𝐹𝑤) ∈ 𝑆) ↔ ((𝜑𝑌 𝑋) → (𝐹𝑌) ∈ 𝑆)))
18 tfrcl.f . . . . . . 7 𝐹 = recs(𝐺)
19 tfrcl.g . . . . . . . 8 (𝜑 → Fun 𝐺)
2019ad2antrl 490 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → Fun 𝐺)
211ad2antrl 490 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → Ord 𝑋)
22 tfrcl.ex . . . . . . . . 9 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
23223adant1r 1231 . . . . . . . 8 (((𝜑𝑤 𝑋) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
24233adant1l 1230 . . . . . . 7 ((((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
25 tfrcl.u . . . . . . . . 9 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
2625adantlr 477 . . . . . . . 8 (((𝜑𝑤 𝑋) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
2726adantll 476 . . . . . . 7 ((((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
28 simprr 531 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → 𝑤 𝑋)
2918, 20, 21, 24, 27, 28tfrcldm 6367 . . . . . 6 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → 𝑤 ∈ dom 𝐹)
3018tfr2a 6325 . . . . . 6 (𝑤 ∈ dom 𝐹 → (𝐹𝑤) = (𝐺‘(𝐹𝑤)))
3129, 30syl 14 . . . . 5 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐹𝑤) = (𝐺‘(𝐹𝑤)))
3219ad2antrl 490 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) → Fun 𝐺)
3332adantr 276 . . . . . . . . . . . . . . 15 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → Fun 𝐺)
3433adantr 276 . . . . . . . . . . . . . 14 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → Fun 𝐺)
351ad2antrl 490 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) → Ord 𝑋)
3635adantr 276 . . . . . . . . . . . . . . 15 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → Ord 𝑋)
3736adantr 276 . . . . . . . . . . . . . 14 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → Ord 𝑋)
38 simplrl 535 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → 𝜑)
3938, 22syl3an1 1271 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
40393adant1r 1231 . . . . . . . . . . . . . 14 (((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
4138, 25sylan 283 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
4241adantlr 477 . . . . . . . . . . . . . 14 (((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
4336, 2syl 14 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → Ord 𝑋)
44 simpr 110 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → 𝑘𝑤)
45 simplrr 536 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → 𝑤 𝑋)
4644, 45jca 306 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → (𝑘𝑤𝑤 𝑋))
47 ordtr1 4390 . . . . . . . . . . . . . . . 16 (Ord 𝑋 → ((𝑘𝑤𝑤 𝑋) → 𝑘 𝑋))
4843, 46, 47sylc 62 . . . . . . . . . . . . . . 15 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → 𝑘 𝑋)
4948adantr 276 . . . . . . . . . . . . . 14 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → 𝑘 𝑋)
5018, 34, 37, 40, 42, 49tfrcldm 6367 . . . . . . . . . . . . 13 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → 𝑘 ∈ dom 𝐹)
5138, 48jca 306 . . . . . . . . . . . . . . 15 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → (𝜑𝑘 𝑋))
5251imim1i 60 . . . . . . . . . . . . . 14 (((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆) → (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → (𝐹𝑘) ∈ 𝑆))
5352impcom 125 . . . . . . . . . . . . 13 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → (𝐹𝑘) ∈ 𝑆)
5450, 53jca 306 . . . . . . . . . . . 12 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆))
5554ex 115 . . . . . . . . . . 11 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → (((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆)))
5655ralimdva 2544 . . . . . . . . . 10 ((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) → (∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆) → ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆)))
5756imp 124 . . . . . . . . 9 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆))
5857an32s 568 . . . . . . . 8 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆))
59 tfrfun 6324 . . . . . . . . . . 11 Fun recs(𝐺)
6018funeqi 5239 . . . . . . . . . . 11 (Fun 𝐹 ↔ Fun recs(𝐺))
6159, 60mpbir 146 . . . . . . . . . 10 Fun 𝐹
6261a1i 9 . . . . . . . . 9 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → Fun 𝐹)
63 ffvresb 5682 . . . . . . . . 9 (Fun 𝐹 → ((𝐹𝑤):𝑤𝑆 ↔ ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆)))
6462, 63syl 14 . . . . . . . 8 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ((𝐹𝑤):𝑤𝑆 ↔ ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆)))
6558, 64mpbird 167 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐹𝑤):𝑤𝑆)
66 vex 2742 . . . . . . 7 𝑤 ∈ V
67 fex 5748 . . . . . . 7 (((𝐹𝑤):𝑤𝑆𝑤 ∈ V) → (𝐹𝑤) ∈ V)
6865, 66, 67sylancl 413 . . . . . 6 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐹𝑤) ∈ V)
69 feq2 5351 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑓:𝑥𝑆𝑓:𝑤𝑆))
7069imbi1d 231 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆)))
7170albidv 1824 . . . . . . 7 (𝑥 = 𝑤 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆)))
72223expia 1205 . . . . . . . . . 10 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
7372alrimiv 1874 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
7473ralrimiva 2550 . . . . . . . 8 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
7574ad2antrl 490 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
7666sucid 4419 . . . . . . . . . 10 𝑤 ∈ suc 𝑤
7776a1i 9 . . . . . . . . 9 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → 𝑤 ∈ suc 𝑤)
78 suceq 4404 . . . . . . . . . . 11 (𝑥 = 𝑤 → suc 𝑥 = suc 𝑤)
7978eleq1d 2246 . . . . . . . . . 10 (𝑥 = 𝑤 → (suc 𝑥𝑋 ↔ suc 𝑤𝑋))
8025ralrimiva 2550 . . . . . . . . . . 11 (𝜑 → ∀𝑥 𝑋 suc 𝑥𝑋)
8180ad2antrl 490 . . . . . . . . . 10 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ∀𝑥 𝑋 suc 𝑥𝑋)
8279, 81, 28rspcdva 2848 . . . . . . . . 9 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → suc 𝑤𝑋)
8377, 82jca 306 . . . . . . . 8 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝑤 ∈ suc 𝑤 ∧ suc 𝑤𝑋))
84 ordtr1 4390 . . . . . . . 8 (Ord 𝑋 → ((𝑤 ∈ suc 𝑤 ∧ suc 𝑤𝑋) → 𝑤𝑋))
8521, 83, 84sylc 62 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → 𝑤𝑋)
8671, 75, 85rspcdva 2848 . . . . . 6 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ∀𝑓(𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆))
87 feq1 5350 . . . . . . . 8 (𝑓 = (𝐹𝑤) → (𝑓:𝑤𝑆 ↔ (𝐹𝑤):𝑤𝑆))
88 fveq2 5517 . . . . . . . . 9 (𝑓 = (𝐹𝑤) → (𝐺𝑓) = (𝐺‘(𝐹𝑤)))
8988eleq1d 2246 . . . . . . . 8 (𝑓 = (𝐹𝑤) → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺‘(𝐹𝑤)) ∈ 𝑆))
9087, 89imbi12d 234 . . . . . . 7 (𝑓 = (𝐹𝑤) → ((𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ((𝐹𝑤):𝑤𝑆 → (𝐺‘(𝐹𝑤)) ∈ 𝑆)))
9190spcgv 2826 . . . . . 6 ((𝐹𝑤) ∈ V → (∀𝑓(𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆) → ((𝐹𝑤):𝑤𝑆 → (𝐺‘(𝐹𝑤)) ∈ 𝑆)))
9268, 86, 65, 91syl3c 63 . . . . 5 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐺‘(𝐹𝑤)) ∈ 𝑆)
9331, 92eqeltrd 2254 . . . 4 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐹𝑤) ∈ 𝑆)
9493exp31 364 . . 3 (𝑤 ∈ On → (∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆) → ((𝜑𝑤 𝑋) → (𝐹𝑤) ∈ 𝑆)))
9512, 17, 94tfis3 4587 . 2 (𝑌 ∈ On → ((𝜑𝑌 𝑋) → (𝐹𝑌) ∈ 𝑆))
966, 7, 95sylc 62 1 (𝜑 → (𝐹𝑌) ∈ 𝑆)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978  wal 1351   = wceq 1353  wcel 2148  wral 2455  Vcvv 2739   cuni 3811  Ord word 4364  Oncon0 4365  suc csuc 4367  dom cdm 4628  cres 4630  Fun wfun 5212  wf 5214  cfv 5218  recscrecs 6308
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-coll 4120  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-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  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-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  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-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-recs 6309
This theorem is referenced by:  rdgon  6390  freccllem  6406  frecfcllem  6408
  Copyright terms: Public domain W3C validator