Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-charfunbi GIF version

Theorem bj-charfunbi 13483
Description: In an ambient set 𝑋, if membership in 𝐴 is stable, then it is decidable if and only if 𝐴 has a characteristic function.

This characterization can be applied to singletons when the set 𝑋 has stable equality, which is the case as soon as it has a tight apartness relation. (Contributed by BJ, 6-Aug-2024.)

Hypotheses
Ref Expression
bj-charfunbi.ex (𝜑𝑋𝑉)
bj-charfunbi.st (𝜑 → ∀𝑥𝑋 STAB 𝑥𝐴)
Assertion
Ref Expression
bj-charfunbi (𝜑 → (∀𝑥𝑋 DECID 𝑥𝐴 ↔ ∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)))
Distinct variable groups:   𝐴,𝑓,𝑥   𝑓,𝑋,𝑥   𝜑,𝑓,𝑥
Allowed substitution hints:   𝑉(𝑥,𝑓)

Proof of Theorem bj-charfunbi
Dummy variables 𝑔 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1w 2218 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
21dcbid 824 . . . 4 (𝑥 = 𝑧 → (DECID 𝑥𝐴DECID 𝑧𝐴))
32cbvralvw 2684 . . 3 (∀𝑥𝑋 DECID 𝑥𝐴 ↔ ∀𝑧𝑋 DECID 𝑧𝐴)
4 eleq1w 2218 . . . . . . . . . . . 12 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
54ifbid 3527 . . . . . . . . . . 11 (𝑧 = 𝑥 → if(𝑧𝐴, 1o, ∅) = if(𝑥𝐴, 1o, ∅))
65cbvmptv 4063 . . . . . . . . . 10 (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) = (𝑥𝑋 ↦ if(𝑥𝐴, 1o, ∅))
76a1i 9 . . . . . . . . 9 ((𝜑 ∧ ∀𝑧𝑋 DECID 𝑧𝐴) → (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) = (𝑥𝑋 ↦ if(𝑥𝐴, 1o, ∅)))
83biimpri 132 . . . . . . . . . 10 (∀𝑧𝑋 DECID 𝑧𝐴 → ∀𝑥𝑋 DECID 𝑥𝐴)
98adantl 275 . . . . . . . . 9 ((𝜑 ∧ ∀𝑧𝑋 DECID 𝑧𝐴) → ∀𝑥𝑋 DECID 𝑥𝐴)
107, 9bj-charfundc 13480 . . . . . . . 8 ((𝜑 ∧ ∀𝑧𝑋 DECID 𝑧𝐴) → ((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)):𝑋⟶2o ∧ (∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = ∅)))
1110ex 114 . . . . . . 7 (𝜑 → (∀𝑧𝑋 DECID 𝑧𝐴 → ((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)):𝑋⟶2o ∧ (∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = ∅))))
12 2on 6375 . . . . . . . . . . 11 2o ∈ On
1312a1i 9 . . . . . . . . . 10 (𝜑 → 2o ∈ On)
14 bj-charfunbi.ex . . . . . . . . . 10 (𝜑𝑋𝑉)
1513, 14elmapd 6610 . . . . . . . . 9 (𝜑 → ((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) ∈ (2o𝑚 𝑋) ↔ (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)):𝑋⟶2o))
1615biimprd 157 . . . . . . . 8 (𝜑 → ((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)):𝑋⟶2o → (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) ∈ (2o𝑚 𝑋)))
1716adantrd 277 . . . . . . 7 (𝜑 → (((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)):𝑋⟶2o ∧ (∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = ∅)) → (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) ∈ (2o𝑚 𝑋)))
1811, 17syld 45 . . . . . 6 (𝜑 → (∀𝑧𝑋 DECID 𝑧𝐴 → (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) ∈ (2o𝑚 𝑋)))
1918imp 123 . . . . 5 ((𝜑 ∧ ∀𝑧𝑋 DECID 𝑧𝐴) → (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) ∈ (2o𝑚 𝑋))
20 fveq1 5470 . . . . . . . . 9 (𝑓 = (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) → (𝑓𝑥) = ((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥))
2120eqeq1d 2166 . . . . . . . 8 (𝑓 = (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) → ((𝑓𝑥) = 1o ↔ ((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = 1o))
2221ralbidv 2457 . . . . . . 7 (𝑓 = (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) → (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ↔ ∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = 1o))
2320eqeq1d 2166 . . . . . . . 8 (𝑓 = (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) → ((𝑓𝑥) = ∅ ↔ ((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = ∅))
2423ralbidv 2457 . . . . . . 7 (𝑓 = (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) → (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅ ↔ ∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = ∅))
2522, 24anbi12d 465 . . . . . 6 (𝑓 = (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅)) → ((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ↔ (∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = ∅)))
2625adantl 275 . . . . 5 (((𝜑 ∧ ∀𝑧𝑋 DECID 𝑧𝐴) ∧ 𝑓 = (𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))) → ((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ↔ (∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = ∅)))
2710simprd 113 . . . . 5 ((𝜑 ∧ ∀𝑧𝑋 DECID 𝑧𝐴) → (∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)((𝑧𝑋 ↦ if(𝑧𝐴, 1o, ∅))‘𝑥) = ∅))
2819, 26, 27rspcedvd 2822 . . . 4 ((𝜑 ∧ ∀𝑧𝑋 DECID 𝑧𝐴) → ∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅))
2928ex 114 . . 3 (𝜑 → (∀𝑧𝑋 DECID 𝑧𝐴 → ∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)))
303, 29syl5bi 151 . 2 (𝜑 → (∀𝑥𝑋 DECID 𝑥𝐴 → ∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)))
31 omex 4555 . . . . . . . . 9 ω ∈ V
32 2ssom 13474 . . . . . . . . 9 2o ⊆ ω
33 mapss 6639 . . . . . . . . 9 ((ω ∈ V ∧ 2o ⊆ ω) → (2o𝑚 𝑋) ⊆ (ω ↑𝑚 𝑋))
3431, 32, 33mp2an 423 . . . . . . . 8 (2o𝑚 𝑋) ⊆ (ω ↑𝑚 𝑋)
35 fveq1 5470 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → (𝑓𝑥) = (𝑔𝑥))
3635eqeq1d 2166 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓𝑥) = 1o ↔ (𝑔𝑥) = 1o))
3736ralbidv 2457 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ↔ ∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = 1o))
3835eqeq1d 2166 . . . . . . . . . . . 12 (𝑓 = 𝑔 → ((𝑓𝑥) = ∅ ↔ (𝑔𝑥) = ∅))
3938ralbidv 2457 . . . . . . . . . . 11 (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅ ↔ ∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = ∅))
4037, 39anbi12d 465 . . . . . . . . . 10 (𝑓 = 𝑔 → ((∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ↔ (∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = ∅)))
4140cbvrexvw 2685 . . . . . . . . 9 (∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) ↔ ∃𝑔 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = ∅))
42 fveqeq2 5480 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑔𝑥) = 1o ↔ (𝑔𝑦) = 1o))
4342cbvralvw 2684 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = 1o ↔ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = 1o)
44 1n0 6382 . . . . . . . . . . . . . . . 16 1o ≠ ∅
4544neii 2329 . . . . . . . . . . . . . . 15 ¬ 1o = ∅
46 eqeq1 2164 . . . . . . . . . . . . . . 15 ((𝑔𝑦) = 1o → ((𝑔𝑦) = ∅ ↔ 1o = ∅))
4745, 46mtbiri 665 . . . . . . . . . . . . . 14 ((𝑔𝑦) = 1o → ¬ (𝑔𝑦) = ∅)
4847neqned 2334 . . . . . . . . . . . . 13 ((𝑔𝑦) = 1o → (𝑔𝑦) ≠ ∅)
4948ralimi 2520 . . . . . . . . . . . 12 (∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = 1o → ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅)
5043, 49sylbi 120 . . . . . . . . . . 11 (∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = 1o → ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅)
51 fveqeq2 5480 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑔𝑥) = ∅ ↔ (𝑔𝑦) = ∅))
5251cbvralvw 2684 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = ∅ ↔ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅)
5352biimpi 119 . . . . . . . . . . 11 (∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = ∅ → ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅)
5450, 53anim12i 336 . . . . . . . . . 10 ((∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = ∅) → (∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅ ∧ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅))
5554reximi 2554 . . . . . . . . 9 (∃𝑔 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑔𝑥) = ∅) → ∃𝑔 ∈ (2o𝑚 𝑋)(∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅ ∧ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅))
5641, 55sylbi 120 . . . . . . . 8 (∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) → ∃𝑔 ∈ (2o𝑚 𝑋)(∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅ ∧ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅))
57 ssrexv 3193 . . . . . . . 8 ((2o𝑚 𝑋) ⊆ (ω ↑𝑚 𝑋) → (∃𝑔 ∈ (2o𝑚 𝑋)(∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅ ∧ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅) → ∃𝑔 ∈ (ω ↑𝑚 𝑋)(∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅ ∧ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅)))
5834, 56, 57mpsyl 65 . . . . . . 7 (∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) → ∃𝑔 ∈ (ω ↑𝑚 𝑋)(∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅ ∧ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅))
5958adantl 275 . . . . . 6 ((𝜑 ∧ ∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)) → ∃𝑔 ∈ (ω ↑𝑚 𝑋)(∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) ≠ ∅ ∧ ∀𝑦 ∈ (𝑋𝐴)(𝑔𝑦) = ∅))
6059bj-charfunr 13482 . . . . 5 ((𝜑 ∧ ∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)) → ∀𝑦𝑋 DECID ¬ 𝑦𝐴)
6160ex 114 . . . 4 (𝜑 → (∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) → ∀𝑦𝑋 DECID ¬ 𝑦𝐴))
62 eleq1w 2218 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
6362notbid 657 . . . . . 6 (𝑥 = 𝑦 → (¬ 𝑥𝐴 ↔ ¬ 𝑦𝐴))
6463dcbid 824 . . . . 5 (𝑥 = 𝑦 → (DECID ¬ 𝑥𝐴DECID ¬ 𝑦𝐴))
6564cbvralvw 2684 . . . 4 (∀𝑥𝑋 DECID ¬ 𝑥𝐴 ↔ ∀𝑦𝑋 DECID ¬ 𝑦𝐴)
6661, 65syl6ibr 161 . . 3 (𝜑 → (∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) → ∀𝑥𝑋 DECID ¬ 𝑥𝐴))
67 bj-charfunbi.st . . . . . 6 (𝜑 → ∀𝑥𝑋 STAB 𝑥𝐴)
6867r19.21bi 2545 . . . . 5 ((𝜑𝑥𝑋) → STAB 𝑥𝐴)
69 stdcn 833 . . . . 5 (STAB 𝑥𝐴 ↔ (DECID ¬ 𝑥𝐴DECID 𝑥𝐴))
7068, 69sylib 121 . . . 4 ((𝜑𝑥𝑋) → (DECID ¬ 𝑥𝐴DECID 𝑥𝐴))
7170ralimdva 2524 . . 3 (𝜑 → (∀𝑥𝑋 DECID ¬ 𝑥𝐴 → ∀𝑥𝑋 DECID 𝑥𝐴))
7266, 71syld 45 . 2 (𝜑 → (∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅) → ∀𝑥𝑋 DECID 𝑥𝐴))
7330, 72impbid 128 1 (𝜑 → (∀𝑥𝑋 DECID 𝑥𝐴 ↔ ∃𝑓 ∈ (2o𝑚 𝑋)(∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋𝐴)(𝑓𝑥) = ∅)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  STAB wstab 816  DECID wdc 820   = wceq 1335  wcel 2128  wne 2327  wral 2435  wrex 2436  Vcvv 2712  cdif 3099  cin 3101  wss 3102  c0 3395  ifcif 3506  cmpt 4028  Oncon0 4326  ωcom 4552  wf 5169  cfv 5173  (class class class)co 5827  1oc1o 6359  2oc2o 6360  𝑚 cmap 6596
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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4085  ax-nul 4093  ax-pow 4138  ax-pr 4172  ax-un 4396  ax-setind 4499  ax-iinf 4550
This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3396  df-if 3507  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-int 3810  df-br 3968  df-opab 4029  df-mpt 4030  df-tr 4066  df-id 4256  df-iord 4329  df-on 4331  df-suc 4334  df-iom 4553  df-xp 4595  df-rel 4596  df-cnv 4597  df-co 4598  df-dm 4599  df-rn 4600  df-res 4601  df-ima 4602  df-iota 5138  df-fun 5175  df-fn 5176  df-f 5177  df-fv 5181  df-ov 5830  df-oprab 5831  df-mpo 5832  df-1o 6366  df-2o 6367  df-map 6598
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator