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

Theorem tfrcl 6034
Description: Closure for transfinite recursion. As with tfr1on 6020, 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 4267 . . . 4 (Ord 𝑋 → Ord 𝑋)
31, 2syl 14 . . 3 (𝜑 → Ord 𝑋)
4 tfrcl.yx . . 3 (𝜑𝑌 𝑋)
5 ordelon 4166 . . 3 ((Ord 𝑋𝑌 𝑋) → 𝑌 ∈ On)
63, 4, 5syl2anc 403 . 2 (𝜑𝑌 ∈ On)
74ancli 316 . 2 (𝜑 → (𝜑𝑌 𝑋))
8 eleq1 2145 . . . . 5 (𝑤 = 𝑘 → (𝑤 𝑋𝑘 𝑋))
98anbi2d 452 . . . 4 (𝑤 = 𝑘 → ((𝜑𝑤 𝑋) ↔ (𝜑𝑘 𝑋)))
10 fveq2 5230 . . . . 5 (𝑤 = 𝑘 → (𝐹𝑤) = (𝐹𝑘))
1110eleq1d 2151 . . . 4 (𝑤 = 𝑘 → ((𝐹𝑤) ∈ 𝑆 ↔ (𝐹𝑘) ∈ 𝑆))
129, 11imbi12d 232 . . 3 (𝑤 = 𝑘 → (((𝜑𝑤 𝑋) → (𝐹𝑤) ∈ 𝑆) ↔ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)))
13 eleq1 2145 . . . . 5 (𝑤 = 𝑌 → (𝑤 𝑋𝑌 𝑋))
1413anbi2d 452 . . . 4 (𝑤 = 𝑌 → ((𝜑𝑤 𝑋) ↔ (𝜑𝑌 𝑋)))
15 fveq2 5230 . . . . 5 (𝑤 = 𝑌 → (𝐹𝑤) = (𝐹𝑌))
1615eleq1d 2151 . . . 4 (𝑤 = 𝑌 → ((𝐹𝑤) ∈ 𝑆 ↔ (𝐹𝑌) ∈ 𝑆))
1714, 16imbi12d 232 . . 3 (𝑤 = 𝑌 → (((𝜑𝑤 𝑋) → (𝐹𝑤) ∈ 𝑆) ↔ ((𝜑𝑌 𝑋) → (𝐹𝑌) ∈ 𝑆)))
18 tfrcl.f . . . . . . 7 𝐹 = recs(𝐺)
19 tfrcl.g . . . . . . . 8 (𝜑 → Fun 𝐺)
2019ad2antrl 474 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → Fun 𝐺)
211ad2antrl 474 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → Ord 𝑋)
22 tfrcl.ex . . . . . . . . 9 ((𝜑𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
23223adant1r 1163 . . . . . . . 8 (((𝜑𝑤 𝑋) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
24233adant1l 1162 . . . . . . 7 ((((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
25 tfrcl.u . . . . . . . . 9 ((𝜑𝑥 𝑋) → suc 𝑥𝑋)
2625adantlr 461 . . . . . . . 8 (((𝜑𝑤 𝑋) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
2726adantll 460 . . . . . . 7 ((((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
28 simprr 499 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → 𝑤 𝑋)
2918, 20, 21, 24, 27, 28tfrcldm 6033 . . . . . 6 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → 𝑤 ∈ dom 𝐹)
3018tfr2a 5991 . . . . . 6 (𝑤 ∈ dom 𝐹 → (𝐹𝑤) = (𝐺‘(𝐹𝑤)))
3129, 30syl 14 . . . . 5 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐹𝑤) = (𝐺‘(𝐹𝑤)))
3219ad2antrl 474 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) → Fun 𝐺)
3332adantr 270 . . . . . . . . . . . . . . 15 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → Fun 𝐺)
3433adantr 270 . . . . . . . . . . . . . 14 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → Fun 𝐺)
351ad2antrl 474 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) → Ord 𝑋)
3635adantr 270 . . . . . . . . . . . . . . 15 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → Ord 𝑋)
3736adantr 270 . . . . . . . . . . . . . 14 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → Ord 𝑋)
38 simplrl 502 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → 𝜑)
3938, 22syl3an1 1203 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
40393adant1r 1163 . . . . . . . . . . . . . 14 (((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ 𝑥𝑋𝑓:𝑥𝑆) → (𝐺𝑓) ∈ 𝑆)
4138, 25sylan 277 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
4241adantlr 461 . . . . . . . . . . . . . 14 (((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ 𝑥 𝑋) → suc 𝑥𝑋)
4336, 2syl 14 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → Ord 𝑋)
44 simpr 108 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → 𝑘𝑤)
45 simplrr 503 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → 𝑤 𝑋)
4644, 45jca 300 . . . . . . . . . . . . . . . 16 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → (𝑘𝑤𝑤 𝑋))
47 ordtr1 4171 . . . . . . . . . . . . . . . 16 (Ord 𝑋 → ((𝑘𝑤𝑤 𝑋) → 𝑘 𝑋))
4843, 46, 47sylc 61 . . . . . . . . . . . . . . 15 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → 𝑘 𝑋)
4948adantr 270 . . . . . . . . . . . . . 14 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → 𝑘 𝑋)
5018, 34, 37, 40, 42, 49tfrcldm 6033 . . . . . . . . . . . . 13 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → 𝑘 ∈ dom 𝐹)
5138, 48jca 300 . . . . . . . . . . . . . . 15 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → (𝜑𝑘 𝑋))
5251imim1i 59 . . . . . . . . . . . . . 14 (((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆) → (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → (𝐹𝑘) ∈ 𝑆))
5352impcom 123 . . . . . . . . . . . . 13 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → (𝐹𝑘) ∈ 𝑆)
5450, 53jca 300 . . . . . . . . . . . 12 ((((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) ∧ ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆))
5554ex 113 . . . . . . . . . . 11 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ 𝑘𝑤) → (((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆)))
5655ralimdva 2434 . . . . . . . . . 10 ((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) → (∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆) → ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆)))
5756imp 122 . . . . . . . . 9 (((𝑤 ∈ On ∧ (𝜑𝑤 𝑋)) ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) → ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆))
5857an32s 533 . . . . . . . 8 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆))
59 tfrfun 5990 . . . . . . . . . . 11 Fun recs(𝐺)
6018funeqi 4972 . . . . . . . . . . 11 (Fun 𝐹 ↔ Fun recs(𝐺))
6159, 60mpbir 144 . . . . . . . . . 10 Fun 𝐹
6261a1i 9 . . . . . . . . 9 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → Fun 𝐹)
63 ffvresb 5381 . . . . . . . . 9 (Fun 𝐹 → ((𝐹𝑤):𝑤𝑆 ↔ ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆)))
6462, 63syl 14 . . . . . . . 8 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ((𝐹𝑤):𝑤𝑆 ↔ ∀𝑘𝑤 (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑆)))
6558, 64mpbird 165 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐹𝑤):𝑤𝑆)
66 vex 2613 . . . . . . 7 𝑤 ∈ V
67 fex 5441 . . . . . . 7 (((𝐹𝑤):𝑤𝑆𝑤 ∈ V) → (𝐹𝑤) ∈ V)
6865, 66, 67sylancl 404 . . . . . 6 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐹𝑤) ∈ V)
69 feq2 5082 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑓:𝑥𝑆𝑓:𝑤𝑆))
7069imbi1d 229 . . . . . . . 8 (𝑥 = 𝑤 → ((𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ (𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆)))
7170albidv 1747 . . . . . . 7 (𝑥 = 𝑤 → (∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ∀𝑓(𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆)))
72223expia 1141 . . . . . . . . . 10 ((𝜑𝑥𝑋) → (𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
7372alrimiv 1797 . . . . . . . . 9 ((𝜑𝑥𝑋) → ∀𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
7473ralrimiva 2439 . . . . . . . 8 (𝜑 → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
7574ad2antrl 474 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ∀𝑥𝑋𝑓(𝑓:𝑥𝑆 → (𝐺𝑓) ∈ 𝑆))
7666sucid 4200 . . . . . . . . . 10 𝑤 ∈ suc 𝑤
7776a1i 9 . . . . . . . . 9 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → 𝑤 ∈ suc 𝑤)
78 suceq 4185 . . . . . . . . . . 11 (𝑥 = 𝑤 → suc 𝑥 = suc 𝑤)
7978eleq1d 2151 . . . . . . . . . 10 (𝑥 = 𝑤 → (suc 𝑥𝑋 ↔ suc 𝑤𝑋))
8025ralrimiva 2439 . . . . . . . . . . 11 (𝜑 → ∀𝑥 𝑋 suc 𝑥𝑋)
8180ad2antrl 474 . . . . . . . . . 10 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ∀𝑥 𝑋 suc 𝑥𝑋)
8279, 81, 28rspcdva 2715 . . . . . . . . 9 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → suc 𝑤𝑋)
8377, 82jca 300 . . . . . . . 8 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝑤 ∈ suc 𝑤 ∧ suc 𝑤𝑋))
84 ordtr1 4171 . . . . . . . 8 (Ord 𝑋 → ((𝑤 ∈ suc 𝑤 ∧ suc 𝑤𝑋) → 𝑤𝑋))
8521, 83, 84sylc 61 . . . . . . 7 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → 𝑤𝑋)
8671, 75, 85rspcdva 2715 . . . . . 6 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → ∀𝑓(𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆))
87 feq1 5081 . . . . . . . 8 (𝑓 = (𝐹𝑤) → (𝑓:𝑤𝑆 ↔ (𝐹𝑤):𝑤𝑆))
88 fveq2 5230 . . . . . . . . 9 (𝑓 = (𝐹𝑤) → (𝐺𝑓) = (𝐺‘(𝐹𝑤)))
8988eleq1d 2151 . . . . . . . 8 (𝑓 = (𝐹𝑤) → ((𝐺𝑓) ∈ 𝑆 ↔ (𝐺‘(𝐹𝑤)) ∈ 𝑆))
9087, 89imbi12d 232 . . . . . . 7 (𝑓 = (𝐹𝑤) → ((𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆) ↔ ((𝐹𝑤):𝑤𝑆 → (𝐺‘(𝐹𝑤)) ∈ 𝑆)))
9190spcgv 2694 . . . . . 6 ((𝐹𝑤) ∈ V → (∀𝑓(𝑓:𝑤𝑆 → (𝐺𝑓) ∈ 𝑆) → ((𝐹𝑤):𝑤𝑆 → (𝐺‘(𝐹𝑤)) ∈ 𝑆)))
9268, 86, 65, 91syl3c 62 . . . . 5 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐺‘(𝐹𝑤)) ∈ 𝑆)
9331, 92eqeltrd 2159 . . . 4 (((𝑤 ∈ On ∧ ∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆)) ∧ (𝜑𝑤 𝑋)) → (𝐹𝑤) ∈ 𝑆)
9493exp31 356 . . 3 (𝑤 ∈ On → (∀𝑘𝑤 ((𝜑𝑘 𝑋) → (𝐹𝑘) ∈ 𝑆) → ((𝜑𝑤 𝑋) → (𝐹𝑤) ∈ 𝑆)))
9512, 17, 94tfis3 4355 . 2 (𝑌 ∈ On → ((𝜑𝑌 𝑋) → (𝐹𝑌) ∈ 𝑆))
966, 7, 95sylc 61 1 (𝜑 → (𝐹𝑌) ∈ 𝑆)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 920  wal 1283   = wceq 1285  wcel 1434  wral 2353  Vcvv 2610   cuni 3621  Ord word 4145  Oncon0 4146  suc csuc 4148  dom cdm 4391  cres 4393  Fun wfun 4946  wf 4948  cfv 4952  recscrecs 5974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3913  ax-sep 3916  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2612  df-sbc 2825  df-csb 2918  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-iun 3700  df-br 3806  df-opab 3860  df-mpt 3861  df-tr 3896  df-id 4076  df-iord 4149  df-on 4151  df-suc 4154  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-f1 4957  df-fo 4958  df-f1o 4959  df-fv 4960  df-recs 5975
This theorem is referenced by:  rdgon  6056  freccllem  6072  frecfcllem  6074
  Copyright terms: Public domain W3C validator